Friedman showed how to turn a classical proof of a formula into an intuitionistic proof of the same formula, thus giving an effective method to extract witnesses from classical proofs of such formulae. In this paper we show how to achieve the same goal efficiently using Krivine realizability with primitive numerals, and prove that the corresponding program is but the direct-style equivalent (using call-cc) of the CPS-style program underlying Friedman's method. © 2009 Springer Berlin Heidelberg.
CITATION STYLE
Miquel, A. (2009). Relating classical realizability and negative translation for existential witness extraction. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5608 LNCS, pp. 188–202). https://doi.org/10.1007/978-3-642-02273-9_15
Mendeley helps you to discover research relevant for your work.