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]. One of the most interesting aspects of the theory is that it is highly modular: although it was originally developed for second order arithmetic, classical realizability naturally extends to more expressive frameworks such as Zermelo-Fraenkel set theory [Kri01] or the calculus of constructions with universes [Miq07]. Moreover, the underlying language of realizers can be freely enriched with new instructions in order to realize extra reasoning principles, such as the axiom of dependent choices [Kri03]. More recently, Krivine [KrilO] proposed an ambitious research programme, whose aim is to unify the methods of classical realizability with Cohen's forcing [Coh63, Coh64] in order to extract programs from proofs obtained by the forcing technique.
展开▼
