A. Abel, Termination checking with types, RAIRO - Theoretical Informatics and Applications, vol.38, issue.4, 2002.
DOI : 10.1051/ita:2004015
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.9.4156

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, Handbook of logic in computer science, 1992.
DOI : 10.1017/cbo9781139032636

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, Journal submission, vol.68, 2003.
URL : https://hal.archives-ouvertes.fr/inria-00105568

F. Blanqui, A short and flexible strong normalization proof for the Calculus of Algebraic Constructions with curried rewriting, 2003.

T. Coquand, Pattern matching with dependent types, Proceedings of the International Workshop on Types for Proofs and Programs, 1992.

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

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

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.
DOI : 10.1007/bfb0020784

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.

R. Pollack, Dependently Typed Records in Type Theory, Formal Aspects of Computing, vol.13, issue.3-5, pp.341-363, 2002.
DOI : 10.1007/s001650200018

C. Development and T. , The Coq Proof Assistant Reference Manual ? Version 7, 2002.

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