M. Abadi, L. Cardelli, P. Curien, and J. Levy, Explicit substitutions, Journal of Functional Programming, vol.4, issue.1, pp.375-416, 1991.
URL : https://hal.archives-ouvertes.fr/inria-00075382

]. P. Acz78 and . Aczel, A general Church-Rosser theorem, 1978.

M. Zena, J. W. Ariola, and . Klop, Equational term graph rewriting, Fundam. Inf, vol.26, issue.3-4, pp.207-240, 1996.

M. Zena, J. W. Ariola, and . Klop, Lambda calculus with explicit recursion, Journal of Information and Computation, vol.139, issue.2, pp.154-233, 1997.

C. [. Asperti and . Laneve, Interaction Systems I: The theory of optimal reductions, Mathematical Structures in Computer Science, vol.690, issue.04, pp.457-504, 1994.
DOI : 10.1007/3-540-56868-9_13

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

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

]. H. Bar92 and . Barendregt, Handbook of Logic in Computer Science, chapter Lambda Calculi with Types, pp.117-309, 1992.

]. L. Bax76 and . Baxter, The Complexity of Unification, 1976.

C. Bertolissi, P. Baldan, H. Cirstea, and C. Kirchner, A Rewriting Calculus for Cyclic Higher-order Term Graphs, Proceedings of TERMGRAPH'04, pp.21-41, 2005.
DOI : 10.1016/j.entcs.2005.01.034

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

H. [. Bertolissi, C. Cirstea, and . Kirchner, Translating Combinatory Reduction Systems into the Rewriting Calculus, Electronic Notes in Theoretical Computer Science, vol.86, issue.2, 2003.
DOI : 10.1016/S1571-0661(04)80674-1

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

G. Barthe, H. Cirstea, C. Kirchner, and L. Liquori, Pure Patterns Type Systems, Principles of Programming Languages -POPL2003, 2003.
URL : https://hal.archives-ouvertes.fr/inria-00099463

P. [. Cherifa and . Lescanne, Termination of rewriting systems by polynomial interpretations and its implementation, Science of Computer Programming, vol.9, issue.2, pp.137-160, 1987.
DOI : 10.1016/0167-6423(87)90030-X

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

]. C. Bibliography-[-ber05 and . Bertolissi, The graph rewriting calculus: confluence and expressiveness, Proceedings of ICTCS'05, 2005.

M. [. Barbanera, H. Fernández, and . 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

]. G. Bir35 and . Birkhoff, On the structure of abstract algebras, Proceedings Cambridge Phil. Soc, vol.31, pp.433-454, 1935.

D. [. Benanav, P. Kapur, and . Narendran, Complexity of matching problems, Journal of Symbolic Computation, vol.3, issue.1-2, pp.203-216, 1987.
DOI : 10.1016/S0747-7171(87)80027-5

]. F. Bla01 and . Blanqui, Type Theory and Rewriting, 2001.

]. S. Blo01 and . Blom, Term Graph Rewriting -syntax and semantics, 2001.

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

S. [. Barendsen and . Smetsers, Uniqueness typing for functional languages with graph rewriting semantics, Mathematical Structures in Computer Science, vol.6, issue.6, pp.579-612, 1996.

W. [. Baader and . Snyder, Unification theory, Handbook of Automated Reasoning, volume I, chapter 8, pp.445-532, 2001.

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

H. P. Barendregt, M. C. Van-eekelen, J. R. Glauert, J. R. Kennaway, M. J. Plasmeijer et al., Term graph rewriting, PARLE Parallel Architectures and Languages Europe, pp.141-158, 1987.
DOI : 10.1007/3-540-17945-3_8

F. [. Corradini and . Drewes, (Cyclic) term graph rewriting is adequate for rational parallel term rewriting, 1997.

G. [. Cirstea, C. Faure, and . Kirchner, A rho-calculus of explicit constraint application, Proceedings of the 5th workshop on rewriting logic and applications, 2004.
URL : https://hal.archives-ouvertes.fr/inria-00000628

]. A. Cg99a, F. Corradini, and . Gadducci, An algebraic presentation of term graphs via gsmonoidal categories, 1999.

]. A. Cg99b, F. Corradini, and . Gadducci, Rewriting on cyclic structures: Equivalence of operational and categorical descriptions, Theoretical Informatics and Applications, pp.467-493, 1999.

]. A. Chu41 and . Church, A Formulation of the Simple Theory of Types, Journal of Symbolic Logic, vol.5, pp.56-68, 1941.

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

C. [. Cirstea and . Kirchner, The Rewriting Calculus as a Semantics of ELAN, 4th Asian Computing Science Conference, pp.8-10, 1998.
DOI : 10.1007/3-540-49366-2_7

C. [. Cirstea and . 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

C. [. Cirstea, L. Kirchner, and . 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-00107876

C. [. Cirstea, L. Kirchner, and . Liquori, Rewriting Calculus with(out) Types, Proceedings of WRLA'02, 2002.
DOI : 10.1016/S1571-0661(05)82526-5

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

L. [. Cirstea, B. Liquori, and . Wack, Rewriting Calculus with Fixpoints: Untyped and First-Order Systems, Proc. of Types, International Workshop on Types for Proof and Programs, pp.147-161, 2003.
DOI : 10.1007/978-3-540-24849-1_10

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

]. A. Cor93 and . Corradini, Term rewriting in CT ?, Proceedings of TAPSOFT'93, Theory and Practice of Software Developm ent / 4th International Joint Conference CAAP/FASE, pp.468-484, 1993.

]. B. Cou83 and . Courcelle, Fundamental properties of infinite trees, Theoretical Computer Science, vol.25, issue.2, pp.95-169, 1983.

D. Dill, A. Drexler, A. Hu, and C. Yang, Protocol verification as a hardware design aid, Proceedings 1992 IEEE International Conference on Computer Design: VLSI in Computers & Processors, pp.522-525, 1992.
DOI : 10.1109/ICCD.1992.276232

]. N. Der82 and . Dershowitz, Orderings for term-rewriting systems, Theoretical Computer Science, vol.17, pp.279-301, 1982.

]. A. Deu96 and . Deursen, An Overview of ASF+SDF, Language Prototyping, pp.1-31, 1996.

T. [. Dowek, C. Hardin, F. Kirchner, and . Pfenning, Unification via explicit substitutions: The case of higher-order patterns, Proceedings of JICSLP'96, 1996.
URL : https://hal.archives-ouvertes.fr/inria-00077203

J. [. Dershowitz and . Jouannaud, Rewrite Systems, pp.244-320, 1990.
DOI : 10.1016/B978-0-444-88074-1.50011-1

]. G. Dow92 and . Dowek, Third order matching is decidable, Proceedings of LICS'92, 1992.

H. Ehrig, R. Heckel, M. Korff, M. Löwe, L. Ribeiro et al., Handbook of Graph Grammars and Computing by Graph Transformation, chapter Algebraic Approach to Graph Transformation Part II: Single Pushout Approach and Comparison with Double Pushout Approach, pp.247-312, 1997.

]. G. Fau05 and . Faure, RhomCal: an implementation of the explicit rewriting calculus Available on, 2005.

G. [. Fages and . Huet, Complete sets of unifiers and matchers in equational theories, Theoretical Computer Science, vol.43, issue.2-3, pp.189-200, 1986.
DOI : 10.1016/0304-3975(86)90175-1

D. [. Forest and . Kesner, Expression Reduction Systems with Patterns, Proceedings of Rewriting Techniques and Applications, 14th International Conference, RTA 2003, pp.107-122, 2003.
DOI : 10.1007/3-540-44881-0_9

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

]. M. Fok92 and . Fokkinga, A gentle introduction to category theory ? the calculational approach, Lecture Notes of the STOP 1992 Summerschool on Constructive Algorithmics, pp.1-72, 1992.

V. [. Gallier and . Breazu-tannen, Polymorphic rewriting conserves algebraic strong normalization and confluence, 16th Colloquium Automata, Languages and Programming, pp.137-150

]. S. Ghi96 and . Ghilezan, Generalized finitness of developments in typed lambda calculi, Journal of Automata, Languages and Combinatorics, vol.1, issue.4, pp.247-258, 1996.

Q. Guo, P. Narendran, and D. A. Wolfram, Unification and matching modulo nilpotence, Conference on Automated Deduction, pp.261-274, 1996.
DOI : 10.1007/3-540-61511-3_90

URL : http://www.cs.albany.edu/~dran/my_research/papers/cade96.ps.Z

]. D. Gol81 and . Goldfarb, The undecidability of the second order unification problem, Theoretical Computer Science, vol.13, pp.225-230, 1981.

P. Haase, J. Broekstra, A. Eberhart, and R. Volz, A Comparison of RDF Query Languages, Proceedings of the Third International Semantic Web Conference, 2004.
DOI : 10.1007/978-3-540-30475-3_35

]. J. Hin64 and . Hindley, The Church-Rosser property and a result in combinatory logic, 1964.

]. J. Hin78 and . Hindley, Reductions of residuals are finite. Transactions of the, pp.345-361, 1978.

D. [. Hoffmann and . Plump, Implementing term rewriting by jungle evaluation, Theorique et Applications/Theoretical Informatics and Applications, 1991.
DOI : 10.1051/ita/1991250504451

[. Hindley and J. P. Seldin, Introduction to Combinators and Lambdacalculus, 1986.

]. G. Hue75 and . Huet, A unification algorithm for typed lambda calculus, Theoretical Computer Science, vol.1, issue.1, pp.27-57, 1975.

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

]. G. Hue80 and . Huet, Confluent reductions: Abstract properties and applications to term rewriting systems, Preliminary version in 18th Symposium on Foundations of Computer Science, pp.797-821, 1977.

H. [. Jouannaud and . Kirchner, Completion of a Set of Rules Modulo a Set of Equations, SIAM Journal on Computing, vol.15, issue.4, pp.1155-1194, 1986.
DOI : 10.1137/0215084

[. Jouannaud and C. Kirchner, Solving equations in abstract algebras: A rulebased survey of unification, Computational Logic: Essays in Honor of Alan Robinson, pp.257-321, 1991.

M. [. Jouannaud and . Okada, Abstract data type systems, Theoretical Computer Science, vol.173, issue.2, pp.349-391, 1997.
DOI : 10.1016/S0304-3975(96)00161-2

]. G. Kah87 and . Kahn, Natural semantics, 1987.

]. W. Kah97 and . Kahl, Algebraic graph derivations for graphical calculi, Proceedings of Graph- Theoretic Concepts in Computer Science, Cadenabbia (Como), Italy, pp.224-238, 1996.

]. W. Kah98 and . Kahl, Relational treatment of term graphs with bound variables, Journal of the IGPL, vol.6, issue.2, pp.259-303, 1998.

P. [. Knuth and . Bendix, Simple Word Problems in Universal Algebras, Computational Problems in Abstract Algebra, pp.263-297, 1970.
DOI : 10.1007/978-3-642-81955-1_23

]. R. Ken87 and . Kennaway, On 'on graph rewritings, Theoretical Computer Science, vol.52, issue.12, pp.37-58, 1987.

]. Z. Kha90 and . Khasidashvili, Expression reduction systems, Proceedings of I. Vekua Institute of Applied Mathematics, pp.200-220, 1990.

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

J. R. Kennaway, J. W. Klop, M. R. Sleep, and F. J. De-vries, On the adequacy of graph rewriting for simulating term rewriting, ACM Transactions on Programming Languages and Systems, vol.16, issue.3, pp.493-523, 1994.
DOI : 10.1145/177492.177577

J. R. Kennaway, J. W. Klop, M. R. Sleep, and F. J. De-vries, Transfinite reductions in orthogonal term rewriting systems, Proceedings 4th Conference on Rewriting Techniques and Applications, Como (Italy), 1991. also Report CS-R9041, CWI, 1990.

J. [. Kamin and . Lévy, Attempts for generalizing the recursive path ordering, 1982.

]. J. Klo80 and . Klop, Combinatory Reduction Systems, 1980.

]. J. Klo90 and . Klop, Term Rewriting Systems, Handbook of Logic in Computer Science, 1990.

P. [. Kapur and . Narendran, Complexity of unification problems with associative-commutative operators, Journal of Automated Reasoning, vol.28, issue.2, pp.261-288, 1992.
DOI : 10.1145/322261.322262

V. [. Klop, F. Van-oostrom, and . 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

]. J. Kvovr93, V. Klop, F. Van-oostrom, and . Van-raamsdonk, Combinatory reduction systems: introduction and survey, Theoretical Computer Science, vol.121, pp.279-308, 1993.

]. Y. Laf90 and . Lafont, Interaction nets, POPL '90: Proceedings of the 17th ACM SIGPLAN- SIGACT symposium on Principles of programming languages, pp.95-108, 1990.

]. J. Lam90 and . Lamping, An algorithm for optimal lambda calculus reduction, POPL '90: Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp.16-30, 1990.

]. D. Lan75 and . Lankford, Canonical algebraic simplifications, 1975.

]. D. Lan79 and . Lankford, A unification algorithm for abelian group theory, 1979.

]. C. Lan93 and . Laneve, Optimality and Concurrency in Interaction Systems, 1993.

]. B. Law63 and . Lawvere, Functorial semantics of algebraic theories, Proceedings of the National Academy of Sciences of the United States of America, vol.50, issue.1, pp.869-872, 1963.

]. Lév78 and . Lévy, Réductions correctes et optimales dans le lambda-calcul, 1978.

]. R. Loa and . Loader, The undecidability of ?-definability

]. M. Löw93 and . Löwe, Algebraic approach to single-pushout graph transformation, Theoretical Computer Science, vol.109, issue.12, pp.181-224, 1993.

B. [. Liquori and . Serpette, iRho, Proceedings of the 6th ACM SIGPLAN international conference on Principles and practice of declarative programming , PPDP '04, pp.167-178, 2004.
DOI : 10.1145/1013963.1013983

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

B. [. Liquori and . Wack, The Polymorphic Rewriting-calculus [Type Checking v.s. Type Inference, Proc. of WRLA, 2004.

]. Mel96 and . Melliès, Description Abstraite des Systèmes de Réécriture, 1996.

]. D. Mil91 and . Miller, A logic programming language with lambda-abstraction, function variables , and simple unification, Journal of Logic and Computation, vol.1, issue.4, pp.497-536, 1991.

G. [. Miller and . Nadathur, Higher-order logic programming, Proceedings of the Third International Logic Programming Conference, pp.448-462, 1986.
DOI : 10.1007/3-540-16492-8_94

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

[. Moreau, D. Ringeissen, and M. Vittek, A pattern matching compiler for multiple target languages, Compiler Construction, 12th International Conference, pp.61-76, 2003.
URL : https://hal.archives-ouvertes.fr/inria-00099644

. E. Msb, R. Miller, D. Swick, and . Brickley, Resource description framework (RDF)

]. M. New42 and . Newman, On theories with a combinatorial definition of equivalence, Annals of Math, pp.223-243, 1942.

]. T. Nip91 and . Nipkow, Combining matching algorithms: The regular case, Journal of Symbolic Computation, vol.12, pp.633-653, 1991.

]. T. Nip93 and . Nipkow, Orthogonal higher-order rewrite systems are confluent, Proceedings of the International Conference on Typed La mbda Calculi and Applications, pp.306-317, 1993.

C. [. Nipkow and . Prehofer, Higher-order rewriting and equational reasoning, Automated Deduction ? A Basis for Applications. Volume I: Foundations. Kluwer, 1998.

]. E. Ohl98 and . Ohlebusch, Church-Rosser theorems for abstract reduction modulo an equivalence relation, Proceedings of RTA'98), volume 1379 of Lecture Notes in Computer Science, pp.17-31, 1998.

]. M. Oka89 and . Okada, Strong normalizability for the combined system of the typed Lambdacalculus and an arbitrary convergent term rewrite system, Proceedings of the ACM-SIGSAM 1989, pp.357-363, 1989.

]. V. Pad96 and . Padovani, Filtrage d'ordre supérieur, Thèse de Doctorat d'Université, 1996.

]. B. Pag97 and . Pagano, Des calculs de substitution explicites et de leur application a la compilation des langages fonctionnels, Thèse de Doctorat d'Université, 1997.

]. M. Par90 and . Parigot, Internal labellings in lambda-calculus, Proceedings of Mathematical Foundations of Computer Science MFCS'90, pp.439-445, 1990.

]. M. Par92 and . Parigot, ?µ-calculus: An algorithmic interpretation of classical natural deduction, Proceedings of LPAR'92, pp.190-201, 1992.

]. G. Plo72 and . Plotkin, Building in equational theories, Machine Intelligence, pp.73-90, 1972.

]. D. Plu99 and . Plump, Handbook of Graph Grammars and Computing by Graph Transformation, pp.3-61, 1999.

M. [. Peterson and . Stickel, Complete Sets of Reductions for Some Equational Theories, Journal of the ACM, vol.28, issue.2, pp.233-264, 1981.
DOI : 10.1145/322248.322251

]. Z. Qia93 and . Qian, Linear unification of higher-order patterns

]. C. Rin96 and . Ringeissen, Combining Decision Algorithms for Matching in the Union of Disjoint Equational Theories, Information and Computation, vol.126, issue.2, pp.144-160, 1996.

]. B. Ros73 and . Rosen, Tree-manipulating systems and Church-Rosser theorems, Journal of the ACM, vol.20, issue.1, pp.160-187, 1973.

H. [. Schneider, M. Ehrig, and . Pfender, Graph-grammars -an algebraic approach, IEEE Proceedings of the Fourteenth Annual Symposium on Switching and Automata Theory, pp.167-180, 1973.

M. R. Sleep, M. J. Plasmeijer, and M. C. Van-eekelen, Term graph rewriting: theory and practice, 1993.

]. J. Sta75 and . Staples, Church-Rosser theorems for replacement systems, Algebra and Logic, Lectures Notes in Mathematics, vol.450, pp.291-307, 1975.

]. R. Sta82 and . Statman, Completeness, invariance and lambda-definability, Journal Symbolic Logic, vol.47, issue.1, pp.17-26, 1982.

]. A. Tur37 and . Turing, Computable numbers with an application to the entscheidungsproblem, Proc. London Math. Soc, vol.42, pp.230-65, 1937.

]. D. Tur79 and . Turner, A new implementation technique for applicative languages. Software and Practice and Experience, pp.31-49, 1979.

F. [. Van-oostrom and . Van-raamsdonk, Comparing combinatory reduction systems and higher-order rewrite systems, Higher-Order Algebra, Logic and Term Rewriting (HOA)vR96] F. van Raamsdonk. Confluence and Normalisation of Higher-Order Rewriting, pp.276-304, 1993.
DOI : 10.1007/3-540-58233-9_13

C. Roel and . De-vrijer, A direct proof of the finite developments theorem, Journal Symbolic Logic, vol.50, issue.2, pp.339-343, 1985.

]. B. Wac03 and . Wack, Klop counter example in the rho-calculus. Draft notes, 2003.

]. B. Wac05 and . Wack, Calcul de réécriture : du typage à la déduction, Thèse de Doctorat d'Université, 2005.

]. C. Wad71 and . Wadsworth, Semantics and Pragmatics of the Lambda Calculus, 1971.

]. D. Wol91 and . Wolfram, Rewriting, and equational unification: The higher-order cases

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