F. Barbanera, M. Fernández, and H. Geuvers, Modularity of strong normalization in the algebraic-??-cube, Journal of Functional Programming, vol.7, issue.6, pp.613-660, 1997.
DOI : 10.1017/S095679689700289X

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

F. Blanqui, Termination and confluence of higherorder rewrite systems, Proc. of RTA'00
URL : https://hal.archives-ouvertes.fr/inria-00105556

F. Blanqui, Théorie des Types et Réécriture (Type Theory and Rewriting), 2001.

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

F. Blanqui, J. Jouannaud, and M. Okada, Inductive-data-type systems, Theoretical Computer Science, vol.272, issue.1-2, 2001.
DOI : 10.1016/S0304-3975(00)00347-9
URL : https://hal.archives-ouvertes.fr/inria-00105578

V. Breazu-tannen, Combining algebra and higherorder types, Proc. of LICS'88
DOI : 10.1109/lics.1988.5103

V. Breazu-tannen and J. Gallier, Polymorphic rewriting conserves algebraic strong normalization, Theoretical Computer Science, vol.83, issue.1, pp.3-28, 1991.
DOI : 10.1016/0304-3975(91)90037-3
URL : http://doi.org/10.1016/0304-3975(91)90037-3

T. Coquand and J. Gallier, A proof of strong normalization for the Theory of Constructions using a Kripke-like interpretation, 1990. Paper presented at the 1st Int. Work. on Logical Frameworks but not published in the proceedings

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

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

G. Dowek, T. Hardin, and C. Kirchner, Theorem proving modulo, INRIA Rocquencourt, 1998.
URL : https://hal.archives-ouvertes.fr/hal-01199506

G. Dowek, B. Werner, G. Dowek, and B. Werner, Proof normalization modulo An inconsistent theory modulo defined by a confluent and terminating rewrite system, Proc. of TYPES'98, 2000.

C. Paulin, The Coq Proof Assistant Reference Manual Version 6.3.1, INRIA Rocquencourt, 2000.
URL : https://hal.archives-ouvertes.fr/inria-00069968

J. Girard, Y. Lafont, and P. Taylor, Proofs and Types, 1988.

J. Hsiang, Refutational theorem proving using term-rewriting systems, Artificial Intelligence, vol.25, issue.3, pp.255-300, 1985.
DOI : 10.1016/0004-3702(85)90074-8

J. Jouannaud and M. Okada, Abstract data type systems, Theoretical Computer Science, vol.173, issue.2, pp.349-391, 1997.
DOI : 10.1016/S0304-3975(96)00161-2
URL : http://doi.org/10.1016/s0304-3975(96)00161-2

J. Jouannaud and A. Rubio, The higher-order recursive path ordering, Proceedings. 14th Symposium on Logic in Computer Science (Cat. No. PR00158)
DOI : 10.1109/LICS.1999.782635

J. W. Klop, V. Van-oostrom, and F. Van-raamsdonk, Combinatory reduction systems: introduction and survey, Theoretical Computer Science, vol.121, issue.1-2, pp.279-308, 1993.
DOI : 10.1016/0304-3975(93)90091-7

P. Martin-löf, Intuitionistic type theory, Bibliopolis, 1984.

N. P. Mendler, Inductive Definition in Type Theory, 1987.

C. Paulin-mohring, Inductive definitions in the system Coq rules and properties, Proc. of TLCA'93
DOI : 10.1007/BFb0037116

M. Stefanova, Properties of Typing Systems, 1998.

J. Van, Termination of higher-order rewrite systems, 1994.

V. Van-oostrom, Confluence for Abstract and Higher- Order Rewriting, 1994.

D. Walukiewicz, Termination of rewriting in the Calculus of Constructions, Proc. of LFM'00
DOI : 10.1017/S0956796802004641

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