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

F. Blanqui, Inductive Types in the Calculus of Algebraic Constructions, Fundamenta Informaticae, vol.65, issue.12, pp.61-86, 2005.
DOI : 10.1007/3-540-44904-3_4
URL : https://hal.archives-ouvertes.fr/inria-00105617

T. Coquand and G. Huet, The calculus of constructions, Information and Computation, vol.76, issue.2-3, pp.95-120, 1988.
DOI : 10.1016/0890-5401(88)90005-3
URL : https://hal.archives-ouvertes.fr/inria-00076024

T. Coquand and C. Paulin-mohring, Inductively defined types, Colog'-88, International Conference on Computer Logic, pp.50-66, 1990.
DOI : 10.1007/3-540-52335-9_47

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

N. Oury, Extensionality in the Calculus of Constructions, Proceedings 18th TPHOL, Oxford, UK. LNCS 3603, pp.278-293, 2005.
DOI : 10.1007/11541868_18

M. Stehr, The Open Calculus of Constructions: An equational type theory with dependent types for programming, specification, and interactive theorem proving (part I and II) Fundamenta Informaticae, 2005.

P. Strub, Type Theory and Decision Procedures, 2008.
URL : https://hal.archives-ouvertes.fr/tel-00351837

P. Strub, Coq Modulo Theory, Proceedings, 2007.
DOI : 10.1007/978-3-642-15205-4_40
URL : https://hal.archives-ouvertes.fr/inria-00497404

B. Werner, Une Théorie des Constructions Inductives, 1994.