B. Werner, Une théorie des constructions inductives, 1994.

B. Barras, Verification of the interface of a small proof system in coq, Lecture Notes in Computer Science, vol.1512, pp.28-45, 1996.
DOI : 10.1007/BFb0097785

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

H. Goguen, The metatheory of UTT, TYPES, ser. Lecture Notes in Computer Science, pp.60-82, 1994.
DOI : 10.1007/3-540-60579-7_4

B. Werner, Sets in types, types in sets, TACS, ser, pp.530-346, 1997.
DOI : 10.1007/BFb0014566

F. Blanqui, J. Jouannaud, and P. Strub, Building Decision Procedures in the Calculus of Inductive Constructions, CSL, ser. Lecture Notes in Computer Science, pp.328-342, 2007.
DOI : 10.1007/978-3-540-74915-8_26
URL : https://hal.archives-ouvertes.fr/inria-00160586

P. Strub, Coq modulo theory, " in CSL, ser. Lecture Notes in Computer Science, pp.529-543, 2010.

A. Miquel and B. Werner, The Not So Simple Proof-Irrelevant Model of CC, Lecture Notes in Computer Science, vol.2646, pp.240-258, 2002.
DOI : 10.1007/3-540-39185-1_14

B. Barras and B. Bernardo, The Implicit Calculus of Constructions as a Programming Language with Dependent Types, FoSSaCS, ser. Lecture Notes in Computer Science, R. M. Amadio, vol.4962, pp.365-379, 2008.
DOI : 10.1007/978-3-540-78499-9_26
URL : https://hal.archives-ouvertes.fr/inria-00429543

E. Wsetbrook, A translation to justify higher-order encodings in intensional type theory, Rice University, Tech. Rep, 2010.

J. Jouannaud and H. Kirchner, Completion of a Set of Rules Modulo a Set of Equations, SIAM Journal on Computing, vol.15, issue.4, pp.1155-1194, 1986.
DOI : 10.1137/0215084