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

B. Barras, Auto-validation d'un système de preuves avec familles inductives, 1999.

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

F. Blanqui, J. Jouannaud, and M. Okada, The Calculus of Algebraic Constructions, RTA, pp.301-316, 1999.
DOI : 10.1007/3-540-48685-2_25
URL : https://hal.archives-ouvertes.fr/inria-00105545

F. Blanqui, J. Jouannaud, and P. Strub, Building Decision Procedures in the Calculus of Inductive Constructions, Proceedings 16th CSL 2007, 2007.
DOI : 10.1007/978-3-540-74915-8_26
URL : https://hal.archives-ouvertes.fr/inria-00160586

A. Bouhoula, J. Jouannaud, and J. Meseguer, Specification and proof in membership equational logic, Theoretical Computer Science, vol.236, issue.1-2, pp.35-132, 2000.
DOI : 10.1016/S0304-3975(99)00206-6
URL : https://hal.archives-ouvertes.fr/inria-00099079

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, International Conference on Computer Logic, pp.50-66, 1990.
DOI : 10.1007/3-540-52335-9_47

P. Corbineau, Démonstration automatique en Théorie des Types, 2005.

J. H. Geuvers and M. Nederhof, A modular proof of strong normalization for the calculus of constructions, J. of Functional programming, vol.1, issue.2, pp.155-189, 1991.

E. Giménez, Structural recursive definitions in type theory, Proceedings of ICALP'98, pp.397-408, 1998.
DOI : 10.1007/BFb0055070

G. Gonthier, The four color theorem in Coq, TYPES 2004 International Workshop, 2004.

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

C. Paulin-mohring, Inductive definitions in the system COQ, Typed Lambda Calculi and Applications, pp.328-345, 1993.

N. Shankar, Little engines of proof, Proceedings of the Seventeenth Annual IEEE Symp. on Logic in Computer Science, 2002.

R. E. Shostak, A Practical Decision Procedure for Arithmetic with Function Symbols, Journal of the ACM, vol.26, issue.2, pp.351-360, 1979.
DOI : 10.1145/322123.322137

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, vol.68, issue.12, pp.131-174, 2005.

T. Streicher, Investigations into intensional type theory, 1993.

P. Strub, The Calculus of Congruent Inductive Constructions, 2008.

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