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

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

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

F. Blanqui, Definitions by rewriting in the Calculus of Constructions, Journal version of LICS'01, 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

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, 2005.

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. Hofmann and T. Streicher, The groupoid model refutes uniqueness of identity proofs, Proceedings Ninth Annual IEEE Symposium on Logic in Computer Science, pp.208-212, 1994.
DOI : 10.1109/LICS.1994.316071

G. Nelson and D. C. Oppen, Fast Decision Procedures Based on Congruence Closure, Journal of the ACM, vol.27, issue.2, pp.356-364, 1980.
DOI : 10.1145/322186.322198
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.125.3226

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

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

H. P. Barendregt, Lambda calculi with types, pp.117-309, 1992.

N. Dershowitz and J. P. Jouannaud, Rewrite Systems, pp.243-320, 1990.
DOI : 10.1016/B978-0-444-88074-1.50011-1

P. Courtieu, Normalized Types, Lecture Notes in Computer Science, vol.2142, pp.554-569, 2001.
DOI : 10.1007/3-540-44802-0_39

A. Petcher and A. Stump, Deciding joinability modulo ground equations in operational type theory, Proof Search in Type Theories (PSTT), 2009.

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

F. Barbanera, M. Fernández, and H. Geuvers, Modularity of strong normalization and confluence in the algebraic-lambda-cube, pp.406-415, 1994.

H. P. Barendregt, The Lambda Calculus. Its Syntax and Semantics, 1984.

J. P. 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