A Survey of Classical Realizability
The theory of classical realizability was introduced by Krivine [Kri09] in the middle of the 90’s in order to analyze the computational contents of classical proofs, following the connection between classical reasoning and control operators discovered by Griffin [Gri90]. More than an extension of the theory of intuitionistic realizability, classical realizability is a complete reformulation of the very principles of realizability based on a combination [OS08, Miq10] of Kleene’s realizability [Kle45] with Friedman’s A-translation [Fri78].
- [Gri90]Griffin, T.: A formulae-as-types notion of control. In: Principles of Programming Languages (POPL 1990), pp. 47–58 (1990)Google Scholar
- [Kri09]Krivine, J.-L.: Realizability in classical logic. In: Interactive Models of Computation and Program Behaviour. Panoramas et synthèses, vol. 27, pp. 197–229. Société Mathématique de France (2009)Google Scholar
- [Kri10]Krivine, J.-L.: Realizability algebras: a program to well order R. CoRR, abs/1005.2395 (2010)Google Scholar
- [Miq10]Miquel, A.: Existential witness extraction in classical realizability and via a negative translation. Logical Methods for Computer Science (2010)Google Scholar