A. Abel, Termination checking with types, RAIRO - Theoretical Informatics and Applications, vol.38, issue.4, 2002.
DOI : 10.1051/ita:2004015

F. Barbanera, M. Fernández, and H. Geuvers, Modularity of strong normalization and confluence in the algebraic-??-cube, Proceedings Ninth Annual IEEE Symposium on Logic in Computer Science, 1994.
DOI : 10.1109/LICS.1994.316049

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

F. Blanqui, Definitions by rewriting in the Calculus of Constructions (extended abstract, Proceedings of the 16th IEEE Symposium on Logic in Computer Science, 2001.

F. Blanqui, Théorie des Types et Récriture Available in english as "Type Theory and Rewriting, 2001.

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

V. Breazu-tannen and J. Gallier, Polymorphic Rewriting Conserves Algebraic Strong Normalization, Proceedings of the 16th International Colloquium on Automata, Languages and Programming, 1989.
DOI : 10.1016/0304-3975(91)90037-3
URL : http://doi.org/10.1016/0304-3975(91)90037-3

T. Coquand, An Analysis of Girard's Paradox, Proceedings of the 1st IEEE Symposium on Logic in Computer Science, 1986.

T. Coquand and G. Huet, The Calculus of Constructions, Information and Computation, pp.95-120, 1988.

T. Coquand and C. Paulin-mohring, Inductively defined types, Proceedings of the International Conference on Computer Logic, 1988.
DOI : 10.1007/3-540-52335-9_47

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

P. Dybjer, Abstract, The Journal of Symbolic Logic, vol.49, issue.02, pp.525-549, 2000.
DOI : 10.1017/CBO9780511569807.011

R. Harper and J. Mitchell, Parametricity and variants of Girard's operator, Information Processing Letters, vol.70, issue.1, pp.1-5, 1999.
DOI : 10.1016/S0020-0190(99)00036-8

J. Jouannaud and M. Okada, Executable Higher-Order Algebraic Specification Languages, Proceedings of the 6th IEEE Symposium on Logic in Computer Science, 1991.

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. 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
URL : http://doi.org/10.1016/0304-3975(93)90091-7

R. Matthes, Extensions of System F by Iteration and Primitive Recursion on Monotone Inductive Types, 1998.

C. Mcbride, Dependently typed functional programs and their proofs, 1999.

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

F. Müller, Confluence of the lambda calculus with left-linear algebraic rewriting, Information Processing Letters, vol.41, issue.6, pp.293-299, 1992.
DOI : 10.1016/0020-0190(92)90155-O

R. Nederpelt, Strong Normalization in a Typed Lambda Calculus with Lambda Structured Types, 1973.
DOI : 10.1016/S0049-237X(08)70217-9

M. Okada, Strong Normalizability for the Combined System of the Typed Lambda Calculus and an Arbitrary Convergent Term Rewrite System, Proceedings of the 1989 International Symposium on Symbolic and Algebraic Computation

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

R. Pollack, Dependently typed records in type theory, Formal Aspects of Computing, pp.341-363, 2002.

M. Rusinowitch, On termination of the direct sum of term-rewriting systems, Information Processing Letters, vol.26, issue.2, pp.65-70, 1987.
DOI : 10.1016/0020-0190(87)90039-1
URL : https://hal.archives-ouvertes.fr/inria-00075874

M. Stefanova, Properties of Typing Systems, 1998.

Y. Toyama, Counterexamples to termination for the direct sum of term rewriting systems, Information Processing Letters, vol.25, issue.3, pp.141-143, 1987.
DOI : 10.1016/0020-0190(87)90122-0

?. Walukiewicz-chrz and D. Aszcz, Termination of rewriting in the Calculus of Constructions, Journal of Functional Programming, vol.13, issue.2, pp.339-414, 2003.

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