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

U. Berger and H. Schwichtenberg, An inverse of the evaluation functional for typed ?calculus, Proceedings of the Sixth Annual IEEE Symposium on Logic in Computer Science, p.203211, 1991.

R. Bonichon and O. Hermant, On Constructive Cut Admissibility in Deduction Modulo, TYPES for proofs and programs, p.3347, 2006.
DOI : 10.1007/978-3-540-74464-1_3
URL : https://hal.archives-ouvertes.fr/hal-01337639

C. Coquand, From semantics to rules: A machine assisted analysis, CSL, p.91105, 1993.
DOI : 10.1007/BFb0049326

O. Danvy, Type-directed partial evaluation, Partial Evaluation -Practice and Theory, DIKU 1998 International Summer School, p.367411, 1998.

H. Herbelin and G. Lee, Formalizing logical metatheory: Semantical cutelimination using kripke models for rst-order predicate logic

O. Hermant and J. Lipton, A Constructive Semantic Approach to Cut Elimination in Type Theories with Axioms, LNCS, vol.5213, p.169183, 2008.
DOI : 10.1007/978-3-540-87531-4_14

D. Ilik, Continuation-passing style models complete for intuitionistic logic, Annals of Pure and Applied Logic, vol.164, issue.6, 2012.
DOI : 10.1016/j.apal.2012.05.003
URL : https://hal.archives-ouvertes.fr/hal-00647390

D. Ilik, G. Lee, and H. Herbelin, Kripke models for classical logic, Annals of Pure and Applied Logic, vol.161, issue.11, p.13671378, 2010.
DOI : 10.1016/j.apal.2010.04.007
URL : https://hal.archives-ouvertes.fr/inria-00371959

J. Krivine, Une preuve formelle et intuitionniste du théorème de complétude de la logique classique. The Bulletin of Symbolic Logic, p.405421, 1996.

S. Maehara, Lattice-valued representation of the cut-elimination theorem, Tsukuba journal of mathematics, vol.15, issue.2, p.509521, 1991.

M. Okada, An Introduction to Linear Logic: Expressiveness and Phase Semantics, MSJ Memoirs, vol.2, p.255295, 1998.
DOI : 10.2969/msjmemoirs/00201C070

M. Okada, Phase semantic cut-elimination and normalization proofs of rstand higher-order linear logic, Theoretical Computer Science, vol.227, p.333396, 1999.

H. Rasiowa and R. Sikorski, The mathematics of metamathematics, 1963.

W. W. Tait, A non constructive proof of gentzen's hauptsatz for second order logic, Bulletin of the AMS, vol.72, p.980983, 1966.

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