F. Baader and K. Schulz, Unification in the union of disjoint equational theories: Combining decision procedures, Proc. 11th Int. Conf. on Automated Deduction, 1992.

H. Barendregt, Lambda calculi with types, volume 2 of Handbook of logic in computer science, 1992.

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

G. Barthe, The relevance of proof-irrelevance, Proc. 24th Int. Coll. on Automata, Languages and Programming LNCS 1443, 1998.
DOI : 10.1007/BFb0055099

F. Blanqui, Type Theory and Rewriting, 2001.
URL : https://hal.archives-ouvertes.fr/inria-00105525

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

. Th, C. Coquand, and . Paulin-mohring, Inductively defined types, Colog'-88, International Conference on Computer Logic, pp.50-66, 1990.

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

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.

M. Hofmann and T. Streicher, The groupoid interpretation of type theory In Twenty-five years of constructive type theory, of Oxford Logic Guides, pp.83-111, 1998.

N. Oury, Extensionality in the Calculus of Constructions, Lecture Notes in Computer Science, vol.3603, pp.278-293, 2005.
DOI : 10.1007/11541868_18

M. Schmidt-schauß, Unification in a combination of arbitrary disjoint equational theories, Journal of Symbolic Computation, vol.8, issue.1-2, pp.51-99, 1989.
DOI : 10.1016/S0747-7171(89)80022-7

N. Shankar, Little engines of proof, Proceedings of the Seventeenth Annual IEEE Symp. on Logic in Computer Science, LICS 2002, 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. O. Stehr, The Open Calculus of Constructions: An equational type theory with dependent types for programming, specification, and interactive theorem proving (part I and II), 2007.

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

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