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

C. Coquand, From semantics to rules: A machine assisted analysis, Lecture Notes in Computer Science, vol.832, pp.91-105, 1993.
DOI : 10.1007/BFb0049326

U. Berger, M. Eberl, and H. Schwichtenberg, Normalization by Evaluation, Lecture Notes in Computer Science, vol.1546, pp.117-137, 1998.
DOI : 10.1007/3-540-49254-2_4

M. Okada, A uniform semantic proof for cut-elimination and completeness of various first and higher order logics, Theoretical Computer Science, vol.281, issue.1-2, pp.471-498, 2002.
DOI : 10.1016/S0304-3975(02)00024-5

V. Danos, J. B. Joinet, and H. Schellinx, LKQ and LKT: sequent calculi for second order logic based upon dual linear decompositions of the classical implication. In: Advances in Linear Logic, pp.211-224, 1995.

J. Y. Girard, Linear logic, Theoretical Computer Science, vol.50, issue.1, pp.1-102, 1987.
DOI : 10.1016/0304-3975(87)90045-4

URL : https://hal.archives-ouvertes.fr/inria-00075966

M. Parigot, Lambda-mu-calculus: An algorithmic interpretation of classical natural deduction, Logic Programming and Automated Reasoning: International Conference LPAR '92 Proceedings, pp.190-201, 1992.

H. Herbelin, A ??-calculus structure isomorphic to Gentzen-style sequent calculus structure, Lecture Notes in Computer Science, vol.933, pp.61-75, 1994.
DOI : 10.1007/BFb0022247

URL : https://hal.archives-ouvertes.fr/inria-00381525

H. Herbelin, Séquents qu'on calcule: de l'interprétation du calcul des séquents comme calcul de ?-termes et comme calcul de stratégies gagnantes, 1995.

S. Kripke, A completeness theorem in modal logic, The Journal of Symbolic Logic, vol.XIV, issue.01, pp.1-14, 1959.
DOI : 10.2307/2964568

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

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

Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development (Coq'Art: The Calculus of Inductive Constructions). Volume XXV of EATCS Texts in Theoretical Computer Science, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00344237