Sciweavers

87
Voted
CORR
2011
Springer
137views Education» more  CORR 2011»
14 years 4 months ago
Existential witness extraction in classical realizability and via a negative translation
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...
Alexandre Miquel