F. Baader and T. Nipkow, Term Rewriting and all That, 1998.

H. Barendregt, The Lambda-Calculus, its syntax and semantics. Studies in Logic and the Foundation of Mathematics, 1984.

P. Borovansk´yborovansk´y, Le contrôle de la réécriture: ´ etude et implantation d'un formalisme de stratégies, Thèse de Doctorat d'Université, 1998.

P. Borovansky, C. Kirchner, H. Kirchner, and P. Moreau, ELAN from a rewriting logic point of view, Theoretical Computer Science, vol.285, issue.2, pp.155-185, 2002.
DOI : 10.1016/S0304-3975(01)00358-9

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

P. Borovansk´yborovansk´y, C. Kirchner, H. Kirchner, P. Moreau, and C. Ringeissen, An overview of ELAN, Proceedings of the second International Workshop on Rewriting Logic and Applications Electronic Notes in Theoretical Computer Science, 1998.

H. Cirstea, Calcul de réécriture : fondements et applications, Thèse de Doctorat d'Université, 2000.

H. Cirstea and C. Kirchner, Combining higher-order and first-order computation using ?-calculus: Towards a semantics of ELAN, Frontiers of Combining Systems, pp.95-120, 1999.
URL : https://hal.archives-ouvertes.fr/inria-00098808

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, Rewriting Techniques and Applications, 2001.
DOI : 10.1007/3-540-45127-7_8

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

H. Cirstea, C. Kirchner, and L. Liquori, Rewriting Calculus with(out) Types, Workshop on Rewriting Logic and its Applications -WRLA'2002, 2002.
DOI : 10.1016/S1571-0661(05)82526-5

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

H. Cirstea, L. Liquori, and B. Wack, Rewriting Calculus with Fixpoints: Untyped and First-Order Systems, 2003.
DOI : 10.1007/978-3-540-24849-1_10

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

N. Dershowitz and J. Jouannaud, Rewrite Systems, Handbook of Theoretical Computer Science, chapter 6, pp.244-320, 1990.
DOI : 10.1016/B978-0-444-88074-1.50011-1

G. Dowek, T. Hardin, and C. Kirchner, Higher-order unification via explicit substitutions, extended abstract, Proceedings of LICS'95, pp.366-374, 1995.

F. Fages and G. Huet, Complete sets of unifiers and matchers in equational theories, Proceedings Fifth Colloquium on Automata, Algebra and Programming, L'Aquila (Italy), pp.205-220, 1983.
DOI : 10.1007/3-540-12727-5_12

G. Faure and C. Kirchner, Exceptions in the Rewriting Calculus, Proceedings of the RTA conference, pp.66-82, 2002.
DOI : 10.1007/3-540-45610-4_6

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

G. Huet, Résolution d'equations dans les langages d'ordre 1, Thèse de Doctorat d'Etat, 1976.

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

G. Kahn, Natural semantics, Proc. of STACS, pp.22-39, 1987.
DOI : 10.1007/BFb0039592

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

C. Kirchner and H. Kirchner, Rewriting, solving, proving. A preliminary version of a book available at www, 1999.

C. Kirchner, H. Kirchner, and M. Vittek, Designing constraint logic programming languages using computational systems, Principles and Practice of Constraint Programming

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

J. Meseguer, Conditional rewriting logic as a unified model of concurrency, Theoretical Computer Science, vol.96, issue.1, pp.73-155, 1992.
DOI : 10.1016/0304-3975(92)90182-F

A. M. Turing, The ??-function in ??-K-conversion, The Journal of Symbolic Logic, vol.57, issue.04, p.164, 1937.
DOI : 10.1215/S0012-7094-36-00227-2

E. Visser, Z. El-abidine, and . Benaissa, A Core Language for Rewriting, Proceedings of the second International Workshop on Rewriting Logic and Applications Electronic Notes in Theoretical Computer Science, 1998.
DOI : 10.1016/S1571-0661(05)80027-1

M. Vittek, ELAN: Un cadre logique pour le prototypage de langages de programmation avec contraintes, Thèse de Doctorat d'Université, 1994.