Existential witness extraction in classical realizability and via a negative translation

We show how to extract existential witnesses from classical proofs usingKrivine's classical realizability---where classical proofs are interpreted aslambda-terms with the call/cc control operator. We first recall the basicframework of classical realizability (in classical second-order arithmetic) andshow how to extend it with primitive numerals for faster computations. Then weshow how to perform witness extraction in this framework, by discussing severaltechniques depending on the shape of the existential formula. In particular, weshow that in the Sigma01-case, Krivine's witness extraction method reduces toFriedman's through a well-suited negative translation to intuitionisticsecond-order arithmetic. Finally we discuss the advantages of using call/ccrather than a negative translation, especially from the point of view of animplementation.Comment: 52 pages. Accepted in Logical Methods for Computer Science (LMCS), 201