L. Augustsson, Cayenne: A Language with Dependent Types, Proc. of ICFP, pp.239-250, 1998.

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 Calculus: its Syntax and Semantics, 1984.

H. Barendregt, Lambda Calculi with Types, Handbook of Logic in Computer Science, volume II, pp.118-310, 1992.

H. Barendregt and H. Geuvers, Proof-Assistants Using Dependent Type Systems, Handbook of Automated Reasoning, volume II, chapter 18, pp.1149-1238, 2001.
DOI : 10.1016/B978-044450813-3/50020-5

G. Barthe and T. Coquand, An Introduction to Dependent Type Theory, Proc. of Applied Semantics Summer School, 2002.
DOI : 10.1007/3-540-45699-6_1

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

H. Cirstea and C. Kirchner, The rewriting calculus - part II, Logic Journal of IGPL, vol.9, issue.3, pp.427-498, 2001.
DOI : 10.1093/jigpal/9.3.377
URL : https://hal.archives-ouvertes.fr/inria-00100532

H. Cirstea, C. Kirchner, and L. Liquori, Matching Power, Proc. of RTA, pp.77-92, 2001.
DOI : 10.1007/3-540-45127-7_8
URL : https://hal.archives-ouvertes.fr/inria-00099308

H. Cirstea, C. Kirchner, and L. Liquori, The Rho Cube, Proc. of FOSSACS, pp.166-180, 2001.
DOI : 10.1007/3-540-45315-6_11
URL : https://hal.archives-ouvertes.fr/inria-00107877

H. Cirstea, C. Kirchner, and L. Liquori, Rewriting Calculus with(out) Types, Proc. of WRLA, 2002.
DOI : 10.1016/S1571-0661(05)82526-5
URL : https://hal.archives-ouvertes.fr/inria-00100858

T. Coquand, Pattern Matching with Dependent Types, Proc. of Logical Frameworks, pp.66-79, 1992.

G. Dowek, T. Hardin, C. Kirchner, and F. Pfenning, Unification via Explicit Substitutions: The Case of Higher-Order Patterns, Proc. of JICSLP, 1996.
URL : https://hal.archives-ouvertes.fr/inria-00077203

G. Faure and C. Kirchner, Exceptions in the Rewriting Calculus, Proc. of RTA, pp.66-82, 2002.
DOI : 10.1007/3-540-45610-4_6
URL : https://hal.archives-ouvertes.fr/inria-00101011

H. Geuvers and M. J. Nederhof, A Modular Proof of Strong Normalisation for the Calculus of Constructions, Journal of Functional Programming, vol.1, issue.2, pp.155-189, 1991.

]. G. Huet, Résolution d'Equations dans les Langages d'Ordre 1, Thèse de Doctorat d'Etat, 1976.

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

D. Kesner, L. Puel, and V. Tannen, A Typed Pattern Calculus, Information and Computation, vol.124, issue.1, pp.32-61, 1996.
DOI : 10.1006/inco.1996.0004

J. W. Klop, Combinatory Reduction Systems, Mathematical Centre Tracts. CWI, vol.127, 1980.

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

D. Miller, A Logic Programming Language with Lambda-abstraction, Function Variables, and Simple Unification, Proc. of ELP, pp.253-281, 1991.

D. Miller, G. Nadathur, F. Pfenning, and A. Shedrov, Uniform proofs as a foundation for logic programming, Annals of Pure and Applied Logic, vol.51, issue.1-2, pp.125-157, 1991.
DOI : 10.1016/0168-0072(91)90068-W

T. Nipkow and C. Prehofer, Higher-order Rewriting and Equational Reasoning, Automated Deduction ? A Basis for Applications. Volume I: Foundations. Kluwer, 1998.

S. and P. Jones, The Implementation of Functional Programming Languages, 1987.

S. L. , P. Jones, and E. Meijer, Henk: a Typed Intermediate Language, Types in Compilation Workshop, 1997.

C. Schürmann, Automating the Meta-Theory of Deductive Systems, 2000.

M. Takahashi, Parallel reductions in ??-calculus, Journal of Symbolic Computation, vol.7, issue.2, pp.113-123, 1989.
DOI : 10.1016/S0747-7171(89)80045-8

S. Van-bakel, L. Liquori, S. Ronchi-della-rocca, and P. Urzyczyn, Comparing cubes of typed and type assignment systems, Annals of Pure and Applied Logic, vol.86, issue.3, pp.267-303, 1997.
DOI : 10.1016/S0168-0072(96)00036-X
URL : https://hal.archives-ouvertes.fr/hal-01154638

V. Van-oostrom, Lambda Calculus with Patterns, 1990.

D. A. Wolfram, The Clausal Theory of Types, volume 21 of Cambridge Tracts in Theoretical Computer Science, 1993.