H. Barendregt, Lambda calculi with types, Handbook of Logic in Computer Science, 1992.

M. Boespflug, Conception d'un noyau de vérification de preuves pour le lambda-Picalcul modulo, 2011.

M. Boespflug and G. Burel, CoqInE : Translating the calculus of inductive constructions into the ??-calculus modulo, 2012.
URL : https://hal.archives-ouvertes.fr/hal-01126128

M. Boespflug, Q. Carbonneaux, and O. Hermant, The ??-calculus modulo as a universal proof language, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00917845

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

D. Cousineau and G. Dowek, Embedding pure type systems in the lambda-Picalculus modulo, Typed Lambda Calculi and Applications, 2007.

A. Dorra, Equivalence de Curry-Howard entre le lambda-Pi-calcul et la logique intuitionniste, 2011.

G. Dowek, T. Hardin, and C. Kirchner, Theorem proving modulo, Journal of Automated Reasoning, 2003.
URL : https://hal.archives-ouvertes.fr/hal-01199506

G. Dowek and B. Werner, Proof normalization modulo, International Workshop on Types for Proofs and Programs, 1998.
DOI : 10.1007/3-540-48167-2_5

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

H. Geuvers and E. Barendsen, Some logical and syntactical observations concerning the first-order dependent type system ??P, Mathematical Structures in Computer Science, vol.9, issue.4, 1999.
DOI : 10.1017/S0960129599002856

G. Gonthier, Formal proof ? the four colour theorem, Asian Symposium on Computer Mathematics, 2007.

C. Thomas, J. Hales, S. Harrison, T. Mclaughlin, S. Nipkow et al., A revision of the proof of the kepler conjecture, Discrete & Computational Geometry, vol.44, 2010.

R. Harper, F. Honsell, and G. Plotkin, A framework for defining logics, Journal of the ACM, vol.40, issue.1, 1993.
DOI : 10.1145/138027.138060

J. Harrison, Inductive definitions: Automation and application, International Workshop on Higher Order Logic Theorem Proving and Its Applications, 1995.
DOI : 10.1007/3-540-60275-5_66

A. William and . Howard, The formulae?as?types notion of construction, Essays on Combinatory Logic, Lambda Calculus, and Formalism, 1980.

J. Hurd, OpenTheory : Package management for higher order logic theories, Programming Languages for Mechanized Mathematics Systems, 2009.

J. Hurd, Composable packages for higher order logic theories, 2010.

J. Hurd, The OpenTheory Standard Theory Library, Nasa Formal Methods, 2011.
DOI : 10.1007/3-540-60275-5_76

C. Keller and B. Werner, Importing HOL Light into Coq, Interactive Theorem Proving, 2010.
DOI : 10.1007/978-3-642-14052-5_22

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

S. Obua and S. Skalberg, Importing HOL into Isabelle/HOL, International Joint Conference on Automated Reasoning, 2006.
DOI : 10.1007/11814771_27