T. Altenkirch, P. Dybjer, M. Hofmann, and P. J. Scott, Normalization by evaluation for typed lambda calculus with coproducts, Proceedings 16th Annual IEEE Symposium on Logic in Computer Science, pp.303-310, 2001.
DOI : 10.1109/LICS.2001.932506

K. Asai and Y. Kameyama, Polymorphic Delimited Continuations, APLAS, pp.239-254, 2007.
DOI : 10.1007/978-3-540-76637-7_16
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.106.9907

F. Barral, Exceptional NbE for sums, pp.21-30, 2009.

S. Berardi and S. Valentini, Krivine's intuitionistic proof of classical completeness (for countable languages), Annals of Pure and Applied Logic, vol.129, issue.1-3, pp.93-106, 2004.
DOI : 10.1016/j.apal.2004.01.002

U. Berger and P. Oliva, Modified bar recursion and classical dependent choice, Logic Colloquium '01, Proceedings of the Annual European Summer Meeting of the Association for Symbolic Logic, pp.89-107, 2001.
DOI : 10.1017/9781316755860.004
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.21.9474

U. Berger and H. Schwichtenberg, An inverse of the evaluation functional for typed lambda -calculus, [1991] Proceedings Sixth Annual IEEE Symposium on Logic in Computer Science, pp.203-211, 1991.
DOI : 10.1109/LICS.1991.151645

S. Burris and S. Lee, Tarski's High School Identities, The American Mathematical Monthly, vol.100, issue.3, pp.231-236, 1993.
DOI : 10.2307/2324454

C. Coquand, From semantics to rules: A machine assisted analysis, CSL '93, pp.91-105, 1993.
DOI : 10.1007/BFb0049326

C. Coquand, A formalised proof of the soundness and completeness of a simply typed lambda-calculus with explicit substitutions, Higher-Order and Symbolic Computation, vol.15, issue.1, pp.57-90, 2002.
DOI : 10.1023/A:1019964114625

O. Danvy, Type-directed partial evaluation, POPL, pp.242-257, 1996.
DOI : 10.7146/dpb.v24i494.7022
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.103.291

O. Danvy, A call-by-name normalization function for the simply typed lambda-calculus with sums and products. manuscript, 2008.

O. Danvy and A. Filinski, A functional abstraction of typed contexts, 1989.

O. Danvy and A. Filinski, Abstracting control, Proceedings of the 1990 ACM conference on LISP and functional programming , LFP '90, pp.151-160, 1990.
DOI : 10.1145/91556.91622

P. Dybjer and A. Filinski, Normalization and Partial Evaluation, 2002.
DOI : 10.1007/3-540-45699-6_4
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.129.4320

A. Filinski, Representing monads, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '94, pp.446-457, 1994.
DOI : 10.1145/174675.178047

A. Filinski, Normalization by Evaluation for the Computational Lambda-Calculus, Typed Lambda Calculi and Applications, pp.151-165, 2001.
DOI : 10.1007/3-540-45413-6_15

M. P. Fiore, R. D. Cosmo, and V. Balat, Remarks on isomorphisms in typed lambda calculi with empty and sum types
URL : https://hal.archives-ouvertes.fr/hal-00149560

H. Herbelin, An Intuitionistic Logic that Proves Markov's Principle, 2010 25th Annual IEEE Symposium on Logic in Computer Science, pp.11-14, 2010.
DOI : 10.1109/LICS.2010.49
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.168.4521

H. Herbelin and G. Lee, Forcing-Based Cut-Elimination for Gentzen-Style Intuitionistic Sequent Calculus, Lecture Notes in Computer Science, vol.27, issue.2, pp.209-217, 2009.
DOI : 10.1007/978-3-662-07964-5
URL : https://hal.archives-ouvertes.fr/inria-00381554

D. Ilik, Formalisation of completeness for Kripke-CPS models, 2009.

D. Ilik, Constructive Completeness Proofs and Delimited Control, 2010.
URL : https://hal.archives-ouvertes.fr/tel-00529021

D. Ilik, Delimited control operators prove double-negation shift. Annals of Pure and Applied Logic, 2011.
DOI : 10.1016/j.apal.2011.12.008
URL : https://hal.archives-ouvertes.fr/hal-00647389

D. Ilik, G. Lee, and H. Herbelin, Kripke models for classical logic, Special Issue: Classical Logic and Computation, pp.1611367-1378, 2008.
DOI : 10.1016/j.apal.2010.04.007
URL : https://hal.archives-ouvertes.fr/inria-00371959

G. Kreisel, On weak completeness of intuitionistic predicate logic, The Journal of Symbolic Logic, vol.23, issue.02, pp.139-158, 1962.
DOI : 10.1007/BF01447860

S. Kripke, Semantical considerations on modal and intuitionistic logic, Acta Philos. Fennica, vol.16, pp.83-94, 1963.

J. Krivine, Une Preuve Formelle et Intuitionniste du Th??or??me de Compl??tude de la Logique Classique, Bulletin of Symbolic Logic, vol.II, issue.04, pp.405-421, 1996.
DOI : 10.1016/0168-0072(94)90047-7

D. Macedonio and G. Sambin, From meta-level to semantics via reflection: a model for basic logic and its extensions

C. Murthy, Extracting Classical Content from Classical Proofs, 1990.

R. Chetan and . Murthy, Control operators, hierarchies, and pseudo-classical type systems: A-translation at work, Proceedings of the ACM SIGPLAN Workshop on Continuations CW92, pp.49-72, 1992.

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. S. Troelstra and D. Van-dalen, Constructivism in mathematics, of Studies in Logic and the Foundations of Mathematics, 1988.

W. Veldman, An Intuitionistic Completeness Theorem for Intuitionistic Predicate Logic, The Journal of Symbolic Logic, vol.41, issue.1, pp.159-166, 1976.
DOI : 10.2307/2272955

A. J. Wilkie, On exponentiation -a solution to Tarski's high school algebra problem, Mathematical Institute, 2001.