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.

G. Barthe, H. Cirstea, C. Kirchner, and L. Liquori, Pure Pattern Type Systems, The ACM press Proc. of POPL, 2003.

V. Breazu-tannen, Combining algebra and higher-order types, [1988] Proceedings. Third Annual Information Symposium on Logic in Computer Science, pp.82-90, 1988.
DOI : 10.1109/LICS.1988.5103

A. Church, A formulation of the simple theory of types, The Journal of Symbolic Logic, vol.1, issue.02, pp.56-68, 1941.
DOI : 10.2307/2371199

H. Cirstea, Calcul de Réécriture : Fondements et Applications, Thèse de Doctorat d'Université, 2000.

H. Cirstea and C. Kirchner, ?-calculus. Its Syntax and Basic Properties, Proc. of Workshop CCL, 1998.

H. Cirstea and C. Kirchner, An Introduction to the Rewriting Calculus, 1999.

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

L. Damas and R. Milner, Principal type-schemes for functional programs, Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '82, pp.207-212, 1982.
DOI : 10.1145/582153.582176

F. Durán, S. Eker, P. Lincoln, and J. Meseguer, Principles of Mobile Maude, Proc. of ASA/MA, pp.73-85, 2000.
DOI : 10.1007/978-3-540-45347-5_7

S. Eker, Associative-commutative matching via bipartite graph matching, The Computer Journal, vol.38, issue.5, pp.381-399, 1995.
DOI : 10.1093/comjnl/38.5.381

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

M. Felleisen and D. P. Friedman, A syntactic theory of sequential state, Theoretical Computer Science, vol.69, issue.3, pp.243-287, 1989.
DOI : 10.1016/0304-3975(89)90069-8

C. Fournet, G. Gonthier, J. Lévy, L. Maranget, and D. Rémy, A calculus of mobile agents, Proc. of CONCUR, pp.406-421, 1996.
DOI : 10.1007/3-540-61604-7_67

J. Gallier and V. Breazu-tannen, Polymorphic Rewriting Conserves Algebraic Strong Normalization and Confluence, Proc. of ICALP, pp.137-150, 1989.

J. Y. Girard, The system F of variable types, fifteen years later, Theoretical Computer Science, vol.45, pp.159-192, 1986.
DOI : 10.1016/0304-3975(86)90044-7

C. A. Gunter, D. Rémy, and J. G. Riecke, A generalization of exceptions and control in ML-like languages, Proceedings of the seventh international conference on Functional programming languages and computer architecture , FPCA '95, pp.66-82
DOI : 10.1145/224164.224173

J. Hullot, Associative-Commutative Pattern Matching, Proc. of IJCAI, 1979.

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

S. N. Kamin, Inheritance in smalltalk-80: a denotational definition, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '88, pp.80-87, 1988.
DOI : 10.1145/73560.73567

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, 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. Leivant, Polymorphic type inference, Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '83, pp.88-98, 1983.
DOI : 10.1145/567067.567077

L. Liquori, Semantica e Pragmatica di un Linguaggio Funzionale con le Continuazioni Esplicite, Laurea in Science dell'Informazione Italian, 1990.

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.

M. Okada, Strong normalizability for the combined system of the typed lmbda calculus and an arbitrary convergent term rewrite system, Proceedings of the ACM-SIGSAM 1989 international symposium on Symbolic and algebraic computation , ISSAC '89, pp.357-363, 1989.
DOI : 10.1145/74540.74582

F. Pessaux and X. Leroy, Type-based analysis of uncaught exceptions, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '99, pp.340-377, 2000.
DOI : 10.1145/292540.292565

URL : https://hal.archives-ouvertes.fr/hal-01499948

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

G. Plotkin, A Structural Approach to Operational Semantics, 1981.

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.