A. Assaf, G. Burel, R. Cauderlier, D. Delahaye, G. Dowek et al., Dedukti: a logical framework based on the lambda-Picalculus modulo theory, 2016.

A. Assaf, G. Dowek, J. Jouannaud, and J. Liu, Untyped confluence in dependent type theories, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01330955

A. Bauer, G. Gilbert, P. Haselwarter, M. Pretnar, and C. A. Stone, Design and implementation of the andromeda proof assistant, 2016.

F. Blanqui, Definitions by rewriting in the Calculus of Constructions, Mathematical Structures in Computer Science, vol.15, issue.1, pp.37-92, 2005.
DOI : 10.1017/S0960129504004426
URL : https://hal.archives-ouvertes.fr/inria-00105568

A. Brunel, O. Hermant, and C. Houtmann, Orthogonality and Boolean Algebras for Deduction Modulo, Typed Lambda Calculus and Applications, pp.76-90, 2011.
DOI : 10.1007/BFb0064875
URL : https://hal.archives-ouvertes.fr/inria-00563331

H. Cirstea, L. Liquori, and B. Wack, Rewriting Calculus with Fixpoints: Untyped and First-Order Systems, Types, 2003.
DOI : 10.1007/978-3-540-24849-1_10
URL : https://hal.archives-ouvertes.fr/inria-00100113

T. Coquand and G. Huet, The calculus of constructions. Information and Computation, pp.95-120, 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, Truth Values Algebras and Proof Normalization, Types for proofs and programs, pp.110-124, 2007.
DOI : 10.1007/978-3-540-74464-1_8

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

G. Dowek, . Th, C. Hardin, and . 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-1316, 2003.
DOI : 10.1007/BFb0037116

S. Foster and G. Struth, Integrating an Automated Theorem Prover into Agda, NASA Formal Methods, 2011.
DOI : 10.1007/978-3-540-70594-9_15
URL : http://eprints.whiterose.ac.uk/43344/2/nasafm11_front.pdf

H. Geuvers, A short and flexible proof of strong normalization for the calculus of constructions, Types for Proofs and Programs, pp.14-38, 1995.
DOI : 10.1007/3-540-60579-7_2

J. Y. Girard, Interprétation Fonctionnelle etÉliminationet´etÉlimination des Coupures dans l'Arithmétique d'Ordre Supérieur, 1972.

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

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

P. Mellì-es and B. Werner, A generic normalisation proof for pure type systems, Types for Proofs and Programs, pp.254-276, 1998.
DOI : 10.1007/BFb0097796

A. Miquel and B. Werner, The Not So Simple Proof-Irrelevant Model of CC, Types for Proofs and Programs, pp.240-258, 2003.
DOI : 10.1007/3-540-39185-1_14

Q. H. Nguyen, C. Kirchner, and H. Kirchner, External rewriting for skeptical proof assistants, Journal of Automated Reasoning, issue.309, p.29, 2002.
URL : https://hal.archives-ouvertes.fr/inria-00101009

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

M. Parigot, Proofs of strong normalization for second order classical natural deduction, Logic in Computer Science, pp.39-46, 1993.