Existential witness extraction in classical realizability and via a negative translation

Alexandre Miquel

We show how to extract existential witnesses from classical proofs using Krivine's classical realizability---where classical proofs are interpreted as lambda-terms with the call/cc…