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

A. Assaf and G. Burel, Holide: https://www.rocq.inria.fr/deducteam

G. Barthe and H. Geuvers, Modular properties of algebraic type systems, HOA, 1995.
DOI : 10.1007/3-540-61254-8_18

F. Blanqui, Definitions by rewriting in the Calculus of Constructions, MSCS, 2005.
URL : https://hal.archives-ouvertes.fr/inria-00105648

M. Boespflug, Q. Carbonneaux, and O. Hermant, The ??-calculus Modulo as a Universal Proof Language, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00917845

N. G. Bruijn, The mathematical language AUTOMATH, its usage, and some of its extensions, Symposium on Automatic Demonstration, 1970.

G. Burel, A Shallow Embedding of Resolution and Superposition Proofs into the ??-Calculus Modulo, PxTP, 2013.
URL : https://hal.archives-ouvertes.fr/hal-01126321

R. Cauderlier, Focalide: https://www.rocq.inria.fr/deducteam/Focalide

M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-oliet et al., The Maude 2.0 System, RTA, 2003.
DOI : 10.1007/3-540-44881-0_7

G. Dowek and D. Cousineau, Embedding Pure Type Systems in ??-Calculus Modulo, TLCA, 2007.

D. Delahaye, D. Doligez, F. Gilbert, P. Halmagrand, and O. Hermant, Zenon Modulo: When Achilles Outruns the Tortoise Using Deduction Modulo, LPAR, 2013.
DOI : 10.1007/978-3-642-45221-5_20
URL : https://hal.archives-ouvertes.fr/hal-00909784

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

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

L. S. Van-benthem-jutting, J. Mckinna, and R. Pollack, Checking algorithms for Pure Type Systems, Types for Proofs and Programs, 1994.
DOI : 10.1007/3-540-58085-9_71

V. Van-oostrom, Confluence for Abstract and Higher-Order Rewriting, 1994.