P. B. Andrews, A reduction of the axioms for the theory of prepositional types, Fundamenta Mathematicae, vol.52, issue.3, pp.345-35010, 1963.
DOI : 10.4064/fm-52-3-345-350

P. B. Andrews, An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, 1986.
DOI : 10.1007/978-94-015-9934-4

A. Assaf, A Calculus of Constructions with explicit subtyping, Types, LIPICS 39, pp.27-46, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01097401

A. Assaf, A framework for defining computational higher-order logics, 2015.
URL : https://hal.archives-ouvertes.fr/tel-01235303

A. Assaf, G. Burel, R. Cauderlier, D. Delahaye, G. Dowek et al., Dedukti: a Logical Framework based on the lambda-Pi-Calculus Modulo Theory, 2016.

H. Barendregt, Lambda calculi with types, Handbook of Logic in Computer Science, pp.117-309, 1992.
DOI : 10.1017/cbo9781139032636

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

M. Boespflug and &. G. Burel, CoqInE : Translating the Calculus of Inductive Constructions into the lambda-Pi-calculus modulo, Second International Workshop on Proof Exchange for Theorem Proving, pp.44-50, 2012.

]. R. Cauderlier, A Rewrite System for Proof Constructivization, Proceedings of the Eleventh Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP '16, 2017.
DOI : 10.1007/11554554_28
URL : https://hal.archives-ouvertes.fr/hal-01420634

R. Cauderlier and &. C. Dubois, FoCaLiZe and Dedukti to the Rescue for Proof Interoperability, Interactive Theorem Proving, pp.131-14710, 2017.
DOI : 10.1007/11916277_11
URL : https://hal.archives-ouvertes.fr/hal-01670700

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

T. Coquand and &. G. Huet, The Calculus of Constructions. Information and Computation, pp.95-12010, 1988.
URL : https://hal.archives-ouvertes.fr/inria-00076024

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

G. Dowek, On the definition of the classical connectives and quantifiers, 2015.
URL : https://hal.archives-ouvertes.fr/hal-00919437

G. Dowek, T. Hardin, and &. C. Kirchner, HOL-lambda-sigma: an intentional first-order expression of higher-order logic, Mathematical Structures in Computer Science, vol.11, pp.1-2510, 2001.
URL : https://hal.archives-ouvertes.fr/inria-00098847

G. Dowek, T. Hardin, and &. C. Kirchner, Theorem proving modulo, Journal of Automated Reasoning, vol.31, issue.1, pp.33-72, 2003.
DOI : 10.1023/A:1027357912519
URL : https://hal.archives-ouvertes.fr/hal-01199506

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

H. Friedman, Systems of second-order arithmetic with restricted induction, I, II, The Journal of Symbolic Logic, vol.41, issue.2, pp.557-559, 1976.

H. Geuvers, Logics and Type systems, 1993.

H. Geuvers, The Calculus of Constructions and Higher Order Logic, The Curry-Howard isomorphism, Cahiers du Centre de logique 8, pp.139-191, 1995.

F. Gilbert, Automated Constructivization of Proofs, Foundations of Software Science and Computation Structures, Lecture notes in computer science 10203, pp.480-495, 2017.
DOI : 10.1007/s10817-009-9143-8
URL : https://hal.archives-ouvertes.fr/hal-01516788

J. Girard, On the unity of logic, Annals of Pure and Applied Logic, vol.59, issue.3, pp.201-21710, 1993.
DOI : 10.1016/0168-0072(93)90093-S
URL : https://hal.archives-ouvertes.fr/inria-00075095

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

L. Henkin, On Mathematical Induction, The American Mathematical Monthly, vol.67, issue.4, pp.323-33810, 1960.
DOI : 10.2307/2308975

L. Henkin, A theory of prepositional types, Fundamenta Mathematicae, vol.52, issue.3, pp.323-344, 1963.
DOI : 10.4064/fm-52-3-323-344

B. Huffman and &. Kunçar, Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL, Certified Programs and Proofs, pp.131-146, 2013.
DOI : 10.1007/978-3-319-03545-1_9

J. Hurd, M. Bobaru, K. Havelund, G. J. Holzmann, and &. R. Joshi, The OpenTheory Standard Theory Library, NASA Formal Methods, pp.177-191, 2011.
DOI : 10.1007/3-540-60275-5_76
URL : http://www.gilith.com/research/papers/stdlib.pdf

F. Kirchner, A Finite First-Order Theory of Classes, Types for Proofs and Programs, pp.188-202, 2006.
DOI : 10.1007/978-3-540-74464-1_13

A. Leitsch, On proof mining by cut-elimination, All about Proofs, Proofs for All, pp.173-200, 2015.

B. Nordström, K. Petersson, and &. J. Smith, Martin-Löf's type theory, Handbook of Logic in Computer Science, pp.1-37, 2000.

D. Prawitz, Classical versus intuitionistic logic Why is this a Proof?, 2015.

R. Saillard, Type Checking in the Lambda-Pi-Calculus Modulo: Theory and Practice, 2015.

S. G. Simpson, Subsystems of second-order arithmetic, pp.10-1017, 2009.

F. Thiré, Sharing Arithmetic Proofs from Dedukti to HOL, 2017.

T. Zimmermann and &. H. Herbelin, Automatic and Transparent Transfer of Theorems along Isomorphisms in the Coq Proof Assistant. Work in progress session, Conference on Intelligent Computer Mathematics, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01152588