]. H. Références-[-bar84 and . Barendregt, Lambda Calculus : its Syntax and Semantics, 1984.

G. [. Benzaken, A. Castagna, and . Frisch, Cduce : an xml-centric general-purpose language, pp.51-63, 2003.
URL : https://hal.archives-ouvertes.fr/hal-00152619

G. Barthe, H. Cirstea, C. Kirchner, and L. Liquori, Pure Patterns Type Systems, Proc. of POPL, pp.250-261, 2003.
DOI : 10.1145/604131.604152

URL : https://hal.archives-ouvertes.fr/inria-00099463

M. [. Basin, J. Clavel, and . Meseguer, Reflective metalogical frameworks, ACM Transactions on Computational Logic, vol.5, issue.3, pp.528-576, 2004.
DOI : 10.1145/1013560.1013566

]. C. Cas96 and . Castro, Solving Binary CSP using Computational Systems, Proceedings of the first international workshop on rewriting logic, 1996.

E. H. Cirstea, W. Coquery, F. Drabent, C. Fages, L. Kirchner et al., Types for rewerse reasoning and query languages, 2005.
URL : https://hal.archives-ouvertes.fr/hal-01149625

]. H. Ckl01a, C. Cirstea, L. Kirchner, and . Liquori, Matching Power, Proc. of RTA, pp.77-92, 2001.

]. H. Ckl01b, C. Cirstea, L. Kirchner, and . Liquori, The Rho Cube, Proc. of FOSSACS, pp.166-180, 2001.

L. [. Cirstea, B. Liquori, and . Wack, Rewriting Calculus with Fixpoints: Untyped and First-Order Systems, TYPES'03, 2004.
DOI : 10.1007/978-3-540-24849-1_10

URL : https://hal.archives-ouvertes.fr/inria-00100113

P. [. Cirstea, A. Moreau, and . Reilles, Rule-based Programming in Java For Protocol Verification, Workshop on Rewriting Logic and Applications, 2004.
DOI : 10.1016/j.entcs.2004.06.022

URL : https://hal.archives-ouvertes.fr/inria-00100025

]. H. Cur34 and . Curry, Functionality in Combinatory Logic, Proc. Nat. Acad. Sci. U.S.A, pp.584-590, 1934.

R. [. Damas and . 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

J. [. Eker, A. Meseguer, and . Sridharanarayanan, The Maude LTL Model Checker and Its Implementation, SPIN, Lecture Notes in Computer Science, pp.230-234, 2003.
DOI : 10.1007/3-540-44829-2_16

A. [. Futatsugi and . Nakagawa, An Overview of Cafe Project, Proc. of CafeOBJ Workshop, 1996.

]. J. Gog04 and . Goguen, The OBJ Family Home Page Characterization of Typings in Polymorphic Type Discipline, Proceedings of the Third Annual Symposium on Logic in Computer Science, pp.61-70, 1988.

A. [. Hosoya, G. Frisch, and . Castagna, Parametric polymorphism for xml, POPL, pp.50-62, 2005.
DOI : 10.1145/1596527.1596529

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

[. Jouannaud and C. Kirchner, Solving equations in abstract algebras : a rule-based survey of unification, Computational Logic. Essays in honor of Alan Robinson, pp.257-321, 1991.

P. [. Kirchner, A. Moreau, and . Reilles, Formal validation of pattern matching code, Proceedings of the 7th ACM SIGPLAN international conference on Principles and practice of declarative programming , PPDP '05, pp.187-197, 2005.
DOI : 10.1145/1069774.1069792

URL : https://hal.archives-ouvertes.fr/inria-00000701

]. D. Lei83 and . Leivant, Polymorphic Type Inference, Proc. of POPL, pp.88-98, 1983.

B. [. Liquori and . Wack, The Polymorphic Rewriting-calculus, Proceedings of the Fifth International Workshop on Rewriting Logic and Its Application, pp.89-111, 2005.
DOI : 10.1016/j.entcs.2004.06.027

URL : https://hal.archives-ouvertes.fr/inria-00099910

J. [. Martí-oliet and . Meseguer, Rewriting logic: roadmap and bibliography, Theoretical Computer Science, vol.285, issue.2, pp.121-154, 2002.
DOI : 10.1016/S0304-3975(01)00357-7

[. Moreau, C. Ringeissen, and M. Vittek, A Pattern Matching Compiler for Multiple Target Languages, 12th Conference on Compiler Construction, pp.61-76, 2003.
URL : https://hal.archives-ouvertes.fr/inria-00099427

R. Milner, M. Tofte, R. Harper, and D. Macqueen, The Definition of Standard ML (Revised), 1997.

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

]. F. Pot and . Pottier, Course DEA : Typage et programmation. http://pauillac.inria.fr/ ~fpottier/mpri/dea-typage.ps.gz, Rém02] D. Rémy. Using, Understanding, and Unraveling the OCaml Language. In Applied Semantics. Advanced Lectures. LNCS 2395, pp.413-537, 2002.

]. J. [-rob65 and . Robinson, A machine-oriented logic based on the resolution principle, journal of the ACM, vol.12, pp.23-41, 1965.

]. M. Van-den-brand, P. Klint, and C. Verhoef, Core technologies for system renovation, SOFSEM : Theory and Practice of Informatics, 23rd Seminar on Current Trends in Theory and Practice of InformaticsvO90] V. van Oostrom. Lambda Calculus with Patterns, pp.235-254, 1990.
DOI : 10.1007/BFb0037407

]. B. Wac05 and . Wack, Typage et déduction dans le calcul de réécriture, Thèse de doctorat, 2005.

]. J. Wel99 and . Wells, Typability and Type Checking in System F are Equivalent and Undecidable, Annals of Pure and Applied Logic, vol.98, pp.1-3111, 1999.