54 search results - page 2 / 11 » Extracting Algorithms from Intuitionistic Proofs |
CORR
2011
Springer
13 years 2 months ago
2011
Springer
Abstract. We show how to extract existential witnesses from classical proofs using Krivine’s classical realizability—where classical proofs are interpreted as λ-terms with the...
LCC
1994
13 years 11 months ago
1994
We demonstrate program extraction by the Light Dialectica Interpretation (LDI) on a minimal logic proof of the classical existence of Fibonacci numbers. This semi-classical proof ...
TPHOL
2003
IEEE
14 years 18 days ago
2003
IEEE
Abstract. It is well known that mathematical proofs often contain (abstract) algorithms, but although these algorithms can be understood by a human, it still takes a lot of time an...
ENTCS
2006
13 years 7 months ago
2006
We formalize two proofs of weak head normalization for the simply typed lambdacalculus in first-order minimal logic: one for normal-order reduction, and one for applicative-order ...
TYPES
2004
Springer
14 years 21 days ago
2004
Springer
We present a formalization of a constructive proof of weak normalization for the simply-typed λ-calculus in the theorem prover Isabelle/HOL, and show how a program can be extracte...