A. Abel, Towards normalization by evaluation for the betaeta-calculus of constructions, FLOPS, pp.224-239, 2010.

[. Abadi, L. Cardelli, P. Curien, and J. Lévy, Abstract, Journal of Functional Programming, vol.34, issue.04, pp.375-416, 1991.
DOI : 10.1016/0304-3975(86)90035-6

[. Abel, T. Coquand, and P. Dybjer, Normalization by evaluation for Martin-Löf Type Theory with typed equality judgements, 22nd IEEE Symposium on Logic in Computer Science, pp.10-12, 2007.

E. Brian, A. Aydemir, B. C. Charguéraud, R. Pierce, S. Pollack et al., Engineering formal metatheory, POPL, pp.3-15, 2008.

A. Adams, Pure type systems with judgemental equality, Journal of Functional Programming, vol.16, issue.02, pp.219-246, 2006.
DOI : 10.1017/S0956796805005770

[. Altenkirch, Constructions, Inductive Types and Strong Normalization, 1993.

B. Barras, Coq contribution: A formalisation of Pure Type Systems

B. Barras, Coq in Sets The Lambda Calculus: its Syntax and Semantics, Sets in Coq of Studies in Logic and the Foundations of Mathematics, 1984.

]. H. Bar92 and . Barendregt, Lambda calculi with types, Handbook of Logic in Computer Science, pp.117-309, 1992.

[. Berardi, Type Dependence and Constructive mathematics, 1988.

[. Barras and B. Werner, Coq in coq, 1997.

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

A. Church, A formulation of the simple theory of types, The Journal of Symbolic Logic, vol.1, issue.02
DOI : 10.2307/2371199

[. Cornes, Conception d'un langage de haut niveau de representation de preuves: Récurrence par filtrage de motifs; Unification en prsence de types inductifs primitifs; Synthèse de lemmes d'inversion, 1997.

[. Cervesato, F. Pfenning, and N. G. De-bruijn, A Linear Spine Calculus, Journal of Logic and Computation, vol.13, issue.5, pp.639-688381, 1972.
DOI : 10.1093/logcom/13.5.639

[. Fangmin, Expansion postponement in pure type systems

A. Felty, A. Martin, R. Crole, and A. Momigliano, Hybrid: a package for higher-order syntax in isabelle and coq

]. Gal and . Gallium, Le langage Caml

[. Geuvers, Logics and Type Systems, 1993.

J. Girard, Une extension de l'interprétation fonctionelle de Gödel l'analyse et son applicationàapplication`applicationà l'´ elimination des coupures dans l'analyse et la théorie des types, Proceedings of the Second Scandinavian Logic Symposium, pp.63-92, 1971.

J. Girard, Interprétation fonctionelle etéliminationetélimination des coupures dans l'arithmétique d'ordre supérieur, 1972.

D. Warren and . Goldfarb, The undecidability of the second-order unification problem, Theor. Comput. Sci, vol.13, pp.225-230, 1981.

F. Gutiérrez and B. C. Ruiz, A Cut-Free Sequent Calculus for Pure Type Systems Verifying the Structural Rules of Gentzen/Kleene, LOPSTR, pp.17-31, 2002.
DOI : 10.1007/3-540-45013-0_2

F. Gutiérrez and B. C. Ruiz, Cut Elimination in a Class of Sequent Calculi for Pure Type Systems, Electronic Notes in Theoretical Computer Science, vol.84, 2003.
DOI : 10.1016/S1571-0661(04)80848-X

H. Geuvers and B. Werner, On the Church-Rosser property for expressive type systems and its consequences for their metatheoretic study, Proceedings Ninth Annual IEEE Symposium on Logic in Computer Science, pp.320-329, 1994.
DOI : 10.1109/LICS.1994.316057

H. Herbelin, A lambda-calculus structure isomorphic to gentzen-style sequent calculus structure, CSL, pp.61-75, 1994.
URL : https://hal.archives-ouvertes.fr/inria-00381525

H. Herbelin, Séquents qu'on calcule, 1995.

]. W. How80 and . Howard, The formulae-as-types notion of construction, pp.479-490, 1980.

B. Huffman and C. Urban, A New Foundation for Nominal Isabelle, ITP, pp.35-50, 2010.
DOI : 10.1007/978-3-642-14052-5_5

P. Gérard and . Huet, Unification in Typed Lambda Calculus, Lambda-Calculus and Computer Science Theory, pp.192-212, 1975.

[. Huet, Constructive computation theory Course notes on lambda calculus, University of Bordeaux I, 2002.

S. Lengrand, Normalisation & Equivalence in Proof Theory & Type Theory, 2006.
URL : https://hal.archives-ouvertes.fr/tel-00134646

]. Z. Luo89 and . Luo, ECC: An extended calculus of constructions, Proceedings of the Fourth Annual Symposium on Logic in computer science, pp.385-395, 1989.

A. Miquel, Le calcul des constructions implicite: syntaxe et sémantique, 2001.

[. Martin-löf, A Theory of Types, 1971.

[. Martin-löf, Intuitionistic Type Theory, Bibliopolis, 1984.

J. Mckinna and R. Pollack, Pure type systems formalized, TLCA, pp.289-305, 1993.
DOI : 10.1007/BFb0037113

J. Mckinna and R. Pollack, Some Lambda Calculus and Type Theory Formalized, BRICS Report Series, vol.4, issue.51, pp.373-409, 1999.
DOI : 10.7146/brics.v4i51.19272

[. Mellì-es and B. Werner, A generic normalization proof for pure type systems, TYPES'96, 1997.

[. Nipkow, L. Paulson, and M. Wenzel, Isabelle Proof Assistant

[. Pfenning, Unification and anti-unification in the calculus of constructions, [1991] Proceedings Sixth Annual IEEE Symposium on Logic in Computer Science, pp.74-85, 1991.
DOI : 10.1109/LICS.1991.151632

]. R. Pol92 and . Pollack, Typechecking in Pure Type Systems, Informal Proceedings of the 1992 Workshop on Types for Proofs and Programs, pp.271-288, 1992.

[. Pollack, The Theory of LEGO: A Proof Checker for the Extended Calculus of Constructions, 1994.

[. Pfenning and C. Schürmann, The twelf project. twelf.plparty.org

[. Siles, Formalization of equivalence between PTS and PTSe

[. Siles, Formalization of sequent calculus pure type system

[. Schack-nielsen and C. Schürmann, The Celf language

[. Streicher, Semantics of type theory: correctness, completeness , and independence results, 1991.
DOI : 10.1007/978-1-4612-0433-6

M. Takahashi, Parallel Reductions in ??-Calculus, Information and Computation, vol.118, issue.1, pp.120-127, 1995.
DOI : 10.1006/inco.1995.1057

]. L. Van-benthem and . Jutting, Typing in pure type systems, Inf. Comput, vol.105, issue.1, pp.30-41, 1993.

]. L. Van-benthem-jutting, J. Mckinna, and R. Pollack, Checking algorithms for Pure Type Systems, TYPES, pp.19-61, 1993.
DOI : 10.1007/3-540-58085-9_71

[. Werner, Une Théorie des Constructions Inductives, 1994.

[. Werner and G. Lee, A simple model of calculus of inductive constructions with judgemental equality