A. Assaf and G. Burel, Translating HOL to Dedukti, Proceedings of the Fourth Workshop on Proof Exchange for Theorem Proving of Electronic Proceedings in Theoretical Computer Science, pp.74-88, 2015.
DOI : 10.4204/EPTCS.186.8

URL : https://hal.archives-ouvertes.fr/hal-01097412

A. Assaf and R. Cauderlier, Mixing HOL and Coq in Dedukti (Extended Abstract), Proceedings of the Fourth Workshop on Proof Exchange for Theorem Proving of Electronic Proceedings in Theoretical Computer Science, pp.89-96, 2015.
DOI : 10.4204/EPTCS.186.9

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

A. Adams, Introducing HOL Zero, Komei Fukuda, Joris van der Hoeven, Michael Joswig, and Nobuki Takayama Mathematical Software ? ICMS 2010, pp.142-143, 2010.
DOI : 10.1007/978-3-642-15582-6_25

A. Adams, The Common HOL Platform, Electronic Proceedings in Theoretical Computer Science, pp.42-56, 2015.
DOI : 10.4204/EPTCS.186.6

B. Peter and . Andrews, An introduction to mathematical logic and type theory: to truth through proof, 1986.

A. W. Appel, Foundational proof-carrying code, 16th Annual IEEE Symposium on Logic in Computer Science, 2001. Proceedings, pp.247-256, 2001.
DOI : 10.1109/lics.2001.932501

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.29.2076

A. Asperti, W. Ricciotti, C. Sacerdoti-coen, and E. Tassi, A compact kernel for the calculus of inductive constructions, Sadhana, vol.174, issue.4, pp.71-144, 2009.
DOI : 10.1007/s12046-009-0003-3

A. Asperti, W. Ricciotti, C. Sacerdoti-coen, and E. Tassi, The Matita Interactive Theorem Prover, Lecture Notes in Computer Science, vol.23, issue.10, pp.64-6910, 2011.
DOI : 10.1007/3-540-48256-3_12

R. D. Arthan, Some mathematical Case Studies in ProofPower-HOL

A. Assaf, A calculus of constructions with explicit subtyping, Postproceedings of the 20th International Conference on Types for Proofs and Programs of Leibniz International Proceedings in Informatics (LIPIcs), pp.27-46, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01097401

A. Assaf, Conservativity of embeddings in the lambda-Pi calculus modulo rewriting, Proceedings of the 13th International Conference on Typed Lambda Calculi and Applications of Leibniz International Proceedings in Informatics (LIPIcs), pp.31-44, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01084165

[. Barendregt, Lambda calculi with types
DOI : 10.1017/cbo9781139032636

B. Barras, Auto-validation d'un système de preuves avec familles inductives, 1999.

M. Boespflug and G. Burel, CoqInE: Translating the calculus of inductive constructions into the lambda-Pi-calculus modulo, Proof Exchange for Theorem Proving?Second International Workshop, p.44, 2012.

Y. Bertot and P. Castéran, Proof by reflection In Interactive Theorem Proving and Program Development, Texts in Theoretical Computer Science An EATCS Series, pp.433-448, 2004.

M. Boespflug, Q. Carbonneaux, and O. Hermant, The lambda-Pi-calculus modulo as a universal proof language, Proof Exchange for Theorem Proving -Second International Workshop, pp.28-43, 2012.

M. Beeson, Foundations of constructive mathematics, 1985.
DOI : 10.1007/978-3-642-68952-9

[. Berardi, Type dependence and constructive mathematics, 1989.

B. Barras and B. Grégoire, On the Role of Type Decorations in the Calculus of Inductive Constructions, Computer Science Logic, number 3634 in Lecture Notes in Computer Science, pp.151-166
DOI : 10.1007/11538363_12

[. Blanqui, Inductive Types in the Calculus of Algebraic Constructions, Typed Lambda Calculi and Applications, pp.46-5910, 2003.
DOI : 10.1007/3-540-44904-3_4

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

[. Blanqui, Definitions by rewriting in the Calculus of Constructions, Mathematical Structures in Computer Science, vol.15, issue.1, pp.37-9210, 2005.
DOI : 10.1017/S0960129504004426

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

G. Burel, A shallow embedding of resolution and superposition proofs into the lambda-Pi-Calculus Modulo, Proceedings of the Third International Workshop on Proof Exchange for Theorem Proving (PxTP), pp.43-57, 2013.

[. Cousineau and G. Dowek, Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo, Typed Lambda Calculi and Applications, pp.102-117, 2007.
DOI : 10.1007/978-3-540-73228-0_9

C. Cauderlier and . Dubois, Objects and subtyping in the lambda-Pi-calculus modulo, Postproceedings of the 20th International Conference on Types for Proofs and Programs of Leibniz International Proceedings in Informatics, pp.47-71, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01126394

M. Coppo and M. Dezani-ciancaglini, A new type assignment for lambda-terms. Archiv für mathematische Logik und Grundlagenforschung, pp.139-156, 1978.

J. Chapman, P. Dagand, C. Mcbride, and P. Morris, The gentle art of levitation, Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming, ICFP '10, pp.3-14, 2010.

[. Coquand and G. Huet, The calculus of constructions Information and Computation, pp.2-395, 1988.

P. Cauderlier and . Halmagrand, Checking Zenon Modulo Proofs in Dedukti, Proceedings of the Fourth Workshop on Proof Exchange for Theorem Proving of Electronic Proceedings in Theoretical Computer Science, pp.57-73, 2015.
DOI : 10.4204/EPTCS.186.7

URL : https://hal.archives-ouvertes.fr/hal-01171360

[. Chihani, Proof certificates for first-order classical and intuitionistic logics

F. Codescu, M. Horozal, T. Kohlhase, F. Mossakowski, and . Rabe, Project Abstract: Logic Atlas and Integrator (LATIN), Intelligent Computer Mathematics, number 6824 in Lecture Notes in Computer Science, pp.289-291, 2011.
DOI : 10.1007/3-540-48660-7_14

F. Codescu, M. Horozal, T. Kohlhase, F. Mossakowski, K. Rabe et al., Towards Logical Frameworks in the Heterogeneous Tool Set Hets, Recent Trends in Algebraic Development Techniques, number 7137 in Lecture Notes in Computer Science, pp.139-159, 2012.
DOI : 10.1007/3-540-48660-7_14

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

[. Chihani and D. Miller, Proof certificates for equality reasoning. Manuscript, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01390919

[. Chihani, D. Miller, and F. Renaud, Foundational Proof Certificates in First-Order Logic, Lecture Notes in Computer Science, vol.7898, pp.24-162, 2013.
DOI : 10.1007/978-3-642-38574-2_11

URL : https://hal.archives-ouvertes.fr/hal-00906485

[. Chihani, D. Miller, and F. Renaud, A semantics for proof evidence In Collected abstracts of Theory and Application of Formal Proofs (LIX Colloquium 2013), pp.36-37

]. T. Coq86 and . Coquand, An analysis of Girard's paradox URL: https, 1986.

[. Coquand, A new paradox in type theory, Proceedings 9th Int. Congress of Logic, pp.555-570, 1991.
DOI : 10.1016/S0049-237X(06)80062-5

. Courant, Explicit Universes for the Calculus of Constructions, Theorem Proving in Higher Order Logics, pp.115-13010, 2002.
DOI : 10.1007/3-540-45685-6_9

[. Cousineau, Models and proof normalization, 2009.
URL : https://hal.archives-ouvertes.fr/tel-00433165

[. Coquand and C. Paulin, Inductively defined types, Lecture Notes in Computer Science, vol.417, issue.88, pp.50-66, 1990.
DOI : 10.1007/3-540-52335-9_47

H. B. Curry, Functionality in Combinatory Logic, Proceedings of the National Academy of Sciences, vol.20, issue.11, pp.584-590, 1934.
DOI : 10.1073/pnas.20.11.584

G. Nicolaas and . De-bruijn, AUTOMATH, a language for mathematics, 1968.

M. Dénès, Propositional extensionality is inconsistent in Coq E-mail communication URL: https://sympa.inria.fr/sympa, pp.2013-2025, 2013.

O. Danvy and A. Filinski, Representing Control: a Study of the CPS Transformation, Mathematical Structures in Computer Science, vol.598, issue.04, pp.361-391, 1992.
DOI : 10.1016/0304-3975(87)90109-5

[. Dowek, T. Hardin, and C. Kirchner, Theorem proving modulo, Journal of Automated Reasoning, vol.31, issue.1, pp.33-7210, 2003.
DOI : 10.1023/A:1027357912519

URL : https://hal.archives-ouvertes.fr/hal-01199506

R. Diaconescu, Axiom of choice and complementation, Proceedings of the American Mathematical Society, pp.176-178, 1975.
DOI : 10.1090/S0002-9939-1975-0373893-X

G. Dowek, Models and termination of proof-reduction in the lambda-Picalculus modulo theory

G. Dowek and B. Werner, An inconsistent theory modulo defined by a confluent and terminating rewrite system. Manuscript URL: https://who, 2000.

G. Dowek and B. Werner, Abstract, The Journal of Symbolic Logic, vol.87, issue.04, pp.1289-1316, 2003.
DOI : 10.1007/BFb0037116

G. Gonthier, A. Asperti, J. Avigad, Y. Bertot, C. Cohen et al., A Machine-Checked Proof of the Odd Order Theorem, Interactive Theorem Proving, pp.163-17910, 2013.
DOI : 10.1007/978-3-642-39634-2_14

URL : https://hal.archives-ouvertes.fr/hal-00816699

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, pp.335-359, 1999.
DOI : 10.1017/S0960129599002856

J. Herman and G. , Logics and type systems, 1993.

E. Giménez, Codifying guarded definitions with recursive schemes, Types for Proofs and Programs, pp.39-5910, 1995.
DOI : 10.1007/3-540-60579-7_3

[. Giménez, Un calcul de constructions infinies et son application a la vérification de systèmes communicants, 1996.

[. Girard, Interprétation fonctionelle et élimination des coupures de l'arithmétique d'ordre supérieur, Thèse de Doctorat, 1972.

[. 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

G. Gonthier and S. Le-roux, An Ssreflect tutorial, Microsoft Research Inria Joint Centre, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00407778

G. Gonthier and A. Mahboubi, An introduction to small scale reflection in Coq, Journal of Formalized Reasoning, vol.3, issue.2, pp.95-152, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00515548

H. Geuvers and M. Nederhof, Modular proof of strong normalization for the calculus of constructions, Journal of Functional Programming, vol.1, issue.2, pp.155-189, 1991.

[. Gonthier, A computer-checked proof of the four colour theorem, 2005.

[. Gonthier, Formal proof?the four-color theorem, Notices of the AMS, vol.55, issue.11, pp.1382-1393, 2008.

C. Thomas and . Hales, The Jordan curve theorem, formally and informally, American Mathematical Monthly, vol.114, issue.10, pp.882-894, 2007.

C. Thomas and . Hales, Announcement of completion URL: https://code.google.com/archive, 2014.

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

J. Harrison, . Hol, and . Light, Overview, Theorem Proving in Higher Order Logics, pp.60-66
DOI : 10.1007/978-1-4302-0821-1_1

URL : https://hal.archives-ouvertes.fr/in2p3-00803620

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, issue.1, pp.1-3410, 2010.

[. Harper, F. Honsell, and G. D. Plotkin, A framework for defining logics, Journal of the ACM, vol.40, issue.1, pp.143-184, 1993.
DOI : 10.1145/138027.138060

A. William and . Howard, The formulae-as-types notion of construction, To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp.479-490, 1980.

R. Harper and R. Pollack, Type checking, universe polymorphism, and typical ambiguity in the calculus of constructions draft, TAPSOFT '89, pp.241-256, 1989.
DOI : 10.1007/3-540-50940-2_39

R. Harper and R. Pollack, Type checking with universes, Theoretical Computer Science, pp.107-13610, 1991.
DOI : 10.1016/0304-3975(90)90108-T

H. Herbelin and A. Spiwack, The rooster and the syntactic bracket, 19th International Conference on Types for Proofs and Programs of Leibniz International Proceedings in Informatics (LIPIcs), pp.169-187, 2013.
URL : https://hal.archives-ouvertes.fr/hal-01097919

O. Hermant and R. Saillard, A rewrite system for strongly normalizable terms, 2015.

A. J. Hurkens, A simplification of Girard's paradox, Typed Lambda Calculi and Applications, pp.266-27810, 1995.
DOI : 10.1007/BFb0014058

J. Hurd, The OpenTheory Standard Theory Library, Lecture Notes in Computer Science, vol.41, issue.1, pp.177-191, 2011.
DOI : 10.1007/3-540-60275-5_76

[. and H. Kirchner, Completion of a set of rules modulo a set of equations, SIAM Journal on Computing, vol.15, issue.4, pp.1155-119410, 1986.

[. Jouannaud, J. Li, and T. Altenkirch, Termination of dependently typed rewrite rules, 13th International Conference on Typed Lambda Calculi and Applications of Leibniz International Proceedings in Informatics (LIPIcs), pp.257-272, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01239083

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

G. Klein, K. Elphinstone, G. Heiser-andronick, D. Cock, P. Derrin et al., seL4, Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles, SOSP '09, pp.207-220, 2009.
DOI : 10.1145/1629575.1629596

[. Kaliszyk and A. Krauss, Scalable LCF-Style Proof Translation, Interactive Theorem Proving, pp.51-66, 2013.
DOI : 10.1007/978-3-642-39634-2_7

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

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

M. Lasson, Réalisabilité et paramétricité dans les systèmes de types purs, 2012.

X. Leroy, The CompCert C verified compiler version 2.5. Manual, Inria, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01091802

Z. Luo, ECC, an extended calculus of constructions, [1989] Proceedings. Fourth Annual Symposium on Logic in Computer Science, pp.386-395, 1989.
DOI : 10.1109/LICS.1989.39193

Z. Luo, ECC, an extended calculus of constructions, [1989] Proceedings. Fourth Annual Symposium on Logic in Computer Science, 1990.
DOI : 10.1109/LICS.1989.39193

Z. Luo, Computation and reasoning: A type theory for computer science. Number 11 in International Series of Monographs on Computer Science, 1994.

[. Muñoz, V. Carreño, G. Dowek, and R. Butler, Formal verification of conflict detection algorithms, International Journal on Software Tools for Technology Transfer (STTT), vol.4, issue.3, pp.371-380, 2003.
DOI : 10.1007/s10009-002-0084-3

[. Martin-löf, An Intuitionistic Theory of Types: Predicative Part, Proceedings of the logic colloquium of Studies in logic and the foundations of mathematics, pp.73-11810, 1973.
DOI : 10.1016/S0049-237X(08)71945-1

P. Martin-löf, Intuitionistic type theory. Notes by Giovanni Sambin of a series of lectures given in Padua, Bibliopolis Naples, 1980.

[. Martin-löf, An intuitionistic theory of types. In Twenty-five years of constructive type theory, pp.127-172, 1998.

T. Mossakowski, C. Maeder, and K. Lüttich, The Heterogeneous Tool Set, Hets, Tools and Algorithms for the Construction and Analysis of Systems, number 4424 in Lecture Notes in Computer Science, pp.519-522, 2007.
DOI : 10.1007/978-3-540-71209-1_40

R. Mayr and T. Nipkow, Higher-order rewrite systems and their confluence, Theoretical Computer Science, vol.192, issue.1, pp.3-2910, 1998.
DOI : 10.1016/S0304-3975(97)00143-6

[. Nipkow, Higher-order critical pairs, [1991] Proceedings Sixth Annual IEEE Symposium on Logic in Computer Science, pp.342-349, 1991.
DOI : 10.1109/LICS.1991.151658

[. Nordström, K. Petersson, and J. M. Smith, Programming in Martin-Löf's type theory. Number 7 in International Series of Monographs on Computer Science, 1990.

M. Naumov, J. Stehr, and . Meseguer, The HOL/NuPRL Proof Translator, Theorem Proving in Higher Order Logics, pp.329-345, 2001.
DOI : 10.1007/3-540-44755-5_23

[. Nipkow, M. Wenzel, and L. C. Paulson, Isabelle/HOL: A Proof Assistant for Higher-order Logic, 2002.
DOI : 10.1007/3-540-45949-9

[. Oury, Coinductive types and type preservation E-mail communication URL: https://sympa.inria.fr/sympa, pp.2008-2014, 2008.

E. Palmgren, On universes in type theory In Twenty-five years of constructive type theory, pp.191-204, 1998.

G. D. Plotkin, Call-by-name, call-by-value and the ??-calculus, Theoretical Computer Science, vol.1, issue.2, pp.125-15910, 1975.
DOI : 10.1016/0304-3975(75)90017-1

F. Pfenning and C. Schürmann, System Description: Twelf ??? A Meta-Logical Framework for Deductive Systems, Automated Deduction ? CADE-16, pp.202-206
DOI : 10.1007/3-540-48660-7_14

[. Rabe, Representing Isabelle in LF, Electronic Proceedings in Theoretical Computer Science, pp.85-99, 2010.
DOI : 10.4204/EPTCS.34.8

[. Rabe, The MMT API: A Generic MKM System, Intelligent Computer Mathematics, number 7961 in Lecture Notes in Computer Science, pp.339-343, 2013.
DOI : 10.1007/978-3-642-39320-4_25

[. Russell, Mathematical Logic as Based on the Theory of Types, American Journal of Mathematics, vol.30, issue.3, pp.222-26210, 1908.
DOI : 10.2307/2369948

[. Saillard, Towards explicit rewrite rules in the lambda-Pi-calculus modulo URL: https, IWIL -10th International Workshop on the Implementation of Logics, 2013.

R. Saillard, Type checking in the lambda-Pi-calculus modulo: theory and practice, École Nationale Supérieure des Mines

V. Siles and H. Herbelin, Pure Type System conversion is always typable, Journal of Functional Programming, vol.1, issue.02, pp.153-180, 2012.
DOI : 10.1017/S0956796805005770

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

J. M. Smith, The independence of Peano's fourth axiom from Martin-L??f's type theory without universes, The Journal of Symbolic Logic, vol.40, issue.03, pp.840-845, 1988.
DOI : 10.1007/BF01180425

K. Slind and M. Norrish, A Brief Overview of HOL4, Theorem Proving in Higher Order Logics, pp.28-32978, 2008.
DOI : 10.1007/s00165-007-0028-5

C. Schürmann and M. Stehr, An Executable Formalization of the HOL/Nuprl Connection in the Metalogical Framework Twelf, 13th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, pp.150-16610, 1007.
DOI : 10.1007/11916277_11

M. Sozeau and N. Tabareau, Universe Polymorphism in Coq, 5th International Conference on Interactive Theorem Proving, pp.499-514, 2014.
DOI : 10.1007/978-3-319-08970-6_32

URL : https://hal.archives-ouvertes.fr/hal-00974721

R. Statman, A new type assignment for strongly normalizable terms, Computer Science Logic 2013 of Leibniz International Proceedings in Informatics (LIPIcs), pp.634-652, 2013.

W. W. Tait, Intensional interpretations of functionals of finite type I. The Journal of Symbolic Logic, pp.198-21210, 1967.

J. Terlouw, Een nadere bewijstheoretische analyse van GSTTs. Manuscript The Netherlands, 1989.

. Vincent-van-oostrom, Confluence for abstract and higher-order rewriting, 1994.

?. We-have and A. B. , By inversion, there exists B such that ?

?. We-have, B. , and }. , By inversion, there exist A , B such that ? M : ?x : A . B and ? N : A and B {x\N } C. By principality (Definition 8.4.3), we have ?x

. Lemma, If ? A ? s and ? A ? s and A A then ?A , s such that A ?? * A and ? A ? s and s s

?. Proof and . ??-*-a, By Lemma 8.1.4, there are two cases to consider. ? If A ? A then by confluence ?A such that A By subject reduction (Lemma 8.2.8), ? A ? s

@. .. Otherwise and . ?x, n . r and r r. By confluence, ?D 1 , . . . , D n such that A ?? * ?x 1 : D 1 . · · · ?x n : D n . r and A ?? * ?x 1 : D 1 . · · · ?x n : D n . r'. By subject reduction (Lemma 8.2.8), ? ?x 1 : D 1 . · · · ?x n : D n . r ? s and ? ?x 1 : D 1 . · · · ?x n : D n . r ? s . By inversion and the local minimum property