L. Allali, Algorithmic Equality in Heyting Arithmetic Modulo, TYPES 2007, Revised Selected Papers, pp.1-17, 2007.
DOI : 10.1007/978-3-540-68103-8_1

Z. Ariola and M. Felleisen, The call-by-need lambda calculus, Journal of Functional Programming, vol.7, issue.3, pp.265-301, 1993.
DOI : 10.1017/S0956796897002724

Z. M. Ariola, P. Downen, H. Herbelin, K. Nakata, and A. Saurin, Classical Call-by-Need Sequent Calculi: The Unity of Semantic Artifacts, Fuji International Symposium on Functional and Logic Programming (FLOPS '12), 2012.
DOI : 10.1007/978-3-642-29822-6_6
URL : https://hal.archives-ouvertes.fr/hal-00697241

Z. M. Ariola, H. Herbelin, and A. Saurin, Classical Call-by-Need and Duality, Typed Lambda Calculi and Applications -10th International Conference, pp.27-44, 2011.
DOI : 10.1017/S096012950000311X
URL : https://hal.archives-ouvertes.fr/inria-00630156

H. P. Barendregt, The Lambda Calculus: Its Syntax and Semantics, 1984.

S. Berardi, M. Bezem, and T. Coquand, Abstract, The Journal of Symbolic Logic, vol.39, issue.02, pp.600-622, 1998.
DOI : 10.1007/BF02007566

U. Berger, A computational interpretation of open induction, Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, 2004., p.326, 2004.
DOI : 10.1109/LICS.2004.1319627

U. Berger and P. Oliva, Modified bar recursion, BRICS, 2002.

A. Church, A set of postulates for the foundation of logic, Annals of Mathematics, vol.2, pp.33-346, 1932.

T. Coquand, A semantics of evidence for classical arithmetic, The Journal of Symbolic Logic, vol.54, issue.01, pp.325-337, 1995.
DOI : 10.1007/BFb0079691

T. Crolard, A confluent ??-calculus with a catch/throw mechanism, Journal of Functional Programming, vol.9, issue.6, pp.625-647, 1999.
DOI : 10.1017/S0956796899003512
URL : https://hal.archives-ouvertes.fr/hal-00094601

P. Curien and H. Herbelin, The duality of computation, Proceedings of ICFP 2000, pp.233-243, 2000.
DOI : 10.1145/357766.351262
URL : https://hal.archives-ouvertes.fr/inria-00156377

A. G. Dragalin, New kinds of realizability and Markov's rule, Soviet Mathematical Doklady, vol.251, pp.534-537, 1980.

M. H. Escardó and P. Oliva, Computational Interpretations of Analysis via Products of Selection Functions, Lecture Notes in Computer Science, vol.6158, pp.141-150, 2010.
DOI : 10.1007/978-3-642-13962-8_16

H. Friedman, Classically and intuitionistically provably recursive functions , " in Higher Set Theory, ser. Lecture Notes in, pp.21-27, 1978.

T. G. 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-57, 1990.
DOI : 10.1145/96709.96714

H. Herbelin, C'est maintenant qu'on calcule: au coeur de la dualité, 2005.

D. Ilik, Preuves constructives de complétude et contrôle délimité, 2010.

S. C. Kleene, On the interpretation of intuitionistic number theory, The Journal of Symbolic Logic, vol.3, issue.04, pp.109-124, 1945.
DOI : 10.1007/BF01565439

J. Krivine, Dependent choice, ???quote??? and the clock, Theoretical Computer Science, vol.308, issue.1-3, pp.259-276, 2003.
DOI : 10.1016/S0304-3975(02)00776-4
URL : https://hal.archives-ouvertes.fr/hal-00154478

J. Maraist, M. Odersky, and P. Wadler, The call-by-need lambda calculus, Journal of Functional Programming, vol.8, issue.3, pp.275-317, 1998.
DOI : 10.1017/S0956796898003037

P. Martin-löf, A theory of types, 1971.

E. Moggi, Computational lambda-calculus and monads, [1989] Proceedings. Fourth Annual Symposium on Logic in Computer Science, 1988.
DOI : 10.1109/LICS.1989.39155

H. Nakano, A constructive formalization of the catch and throw mechanism, [1992] Proceedings of the Seventh Annual IEEE Symposium on Logic in Computer Science, pp.82-89, 1992.
DOI : 10.1109/LICS.1992.185522

C. Okasaki, P. Lee, and D. Tarditi, Call-by-need and continuationpassing style, Lisp and Symbolic Computation, pp.57-82, 1994.

M. Parigot, Free deduction: An analysis of ???Computations??? in classical logic, Proceedings of LPAR, ser. LNCS, A. Voronkov, pp.361-380, 1991.
DOI : 10.1007/3-540-55460-2_27

G. D. Plotkin, Call-by-name, call-by-value and the ??-calculus, Theoretical Computer Science, vol.1, issue.2, pp.125-159, 1975.
DOI : 10.1016/0304-3975(75)90017-1

A. Sabry and M. Felleisen, Reasoning about programs in continuationpassing style, Lisp and Symbolic Computation, pp.289-360, 1993.

A. Sabry and P. Wadler, A reflection on call-by-value, ACM Transactions on Programming Languages and Systems, vol.19, issue.6, pp.916-941, 1997.
DOI : 10.1145/267959.269968

C. Spector, Provably recursive functionals of analysis: a consistency proof of analysis by an extension of principles formulated in current intuitionistic mathematics, Recursive function theory: Proceedings of symposia in pure mathematics, pp.1-27, 1962.
DOI : 10.1090/pspum/005/0154801