H. Barendregt, The Lambda Calculus: Its Syntax and Semantics, volume 103 of Studies in Logic and The Foundations of Mathematics, 1984.

S. Boutin, Using reflection to build efficient and certified decision procedures, TACS'97. Springer-Verlag LNCS 1281, pp.515-529, 1997.
DOI : 10.1007/BFb0014565

A. Church, The calculi of lambda-conversion, Annals of Mathematical Studies. Princeton, vol.6, 1941.

T. Griffin, A formulae-as-type notion of control, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '90, pp.47-58, 1990.
DOI : 10.1145/96709.96714

G. Huet, The Zipper, Journal of Functional Programming, vol.7, issue.5, pp.549-554, 1997.
DOI : 10.1017/S0956796897002864

J. Krivine, A general storage theorem for integers in call-by-name ??-calculus, Theoretical Computer Science, vol.129, issue.1, pp.79-94, 1994.
DOI : 10.1016/0304-3975(94)90081-7

]. Kri03 and . Krivine, Dependent choice, 'quote' and the clock, Theor. Comput. Sci, vol.308, issue.1-3, pp.259-276, 2003.

J. Krivine, Realizability in classical logic In Interactive models of computation and program behaviour, of Panoramas et synthèses, pp.197-229, 2009.

A. Miquel, Classical Program Extraction in the Calculus of Constructions, Computer Science Logic (CSL), pp.313-327, 2007.
DOI : 10.1007/978-3-540-74915-8_25
URL : https://hal.archives-ouvertes.fr/hal-00150889

A. Miquel, The classical extraction module for Coq, 2009.

A. Miquel, De la formalisation des preuvesàpreuvesà l'extraction de programmes, 2009.

A. Miquel, The Jivaro head reduction machine for the ? c -calculus, 2009.

A. Miquel, Existential witness extraction in classical realizability and via a negative translation, Logical Methods in Computer Science (LMCS), 2010.
DOI : 10.2168/LMCS-7(2:2)2011
URL : https://hal.archives-ouvertes.fr/hal-00800560

A. Miquel, The reasonnable effectiveness of mathematical proof, Anachronismes logiques, 2011.