Lambda calculi with types, Handbook of Logic in Computer Science, 1992. ,
Conception d'un noyau de vérification de preuves pour le lambda-Picalcul modulo, 2011. ,
CoqInE : Translating the calculus of inductive constructions into the ??-calculus modulo, 2012. ,
URL : https://hal.archives-ouvertes.fr/hal-01126128
The ??-calculus modulo as a universal proof language, 2012. ,
URL : https://hal.archives-ouvertes.fr/hal-00917845
A formulation of the simple theory of types, The Journal of Symbolic Logic, vol.1, issue.02, 1940. ,
DOI : 10.2307/2371199
Embedding pure type systems in the lambda-Picalculus modulo, Typed Lambda Calculi and Applications, 2007. ,
Equivalence de Curry-Howard entre le lambda-Pi-calcul et la logique intuitionniste, 2011. ,
Theorem proving modulo, Journal of Automated Reasoning, 2003. ,
URL : https://hal.archives-ouvertes.fr/hal-01199506
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
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
Formal proof ? the four colour theorem, Asian Symposium on Computer Mathematics, 2007. ,
A revision of the proof of the kepler conjecture, Discrete & Computational Geometry, vol.44, 2010. ,
A framework for defining logics, Journal of the ACM, vol.40, issue.1, 1993. ,
DOI : 10.1145/138027.138060
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
The formulae?as?types notion of construction, Essays on Combinatory Logic, Lambda Calculus, and Formalism, 1980. ,
OpenTheory : Package management for higher order logic theories, Programming Languages for Mechanized Mathematics Systems, 2009. ,
Composable packages for higher order logic theories, 2010. ,
The OpenTheory Standard Theory Library, Nasa Formal Methods, 2011. ,
DOI : 10.1007/3-540-60275-5_76
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
Importing HOL into Isabelle/HOL, International Joint Conference on Automated Reasoning, 2006. ,
DOI : 10.1007/11814771_27