Explicit substitutions, Journal of Functional Programming, vol.4, issue.1, pp.375-416, 1991. ,
URL : https://hal.archives-ouvertes.fr/inria-00075382
A general Church-Rosser theorem, 1978. ,
Equational term graph rewriting, Fundam. Inf, vol.26, issue.3-4, pp.207-240, 1996. ,
Lambda calculus with explicit recursion, Journal of Information and Computation, vol.139, issue.2, pp.154-233, 1997. ,
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
The Lambda-Calculus, its syntax and semantics. Studies in Logic and the Foundation of Mathematics, 1984. ,
Handbook of Logic in Computer Science, chapter Lambda Calculi with Types, pp.117-309, 1992. ,
The Complexity of Unification, 1976. ,
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
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
Pure Patterns Type Systems, Principles of Programming Languages -POPL2003, 2003. ,
URL : https://hal.archives-ouvertes.fr/inria-00099463
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
The graph rewriting calculus: confluence and expressiveness, Proceedings of ICTCS'05, 2005. ,
Modularity of strong normalization in the algebraic-??-cube, Journal of Functional Programming, vol.7, issue.6, pp.613-660, 1997. ,
DOI : 10.1017/S095679689700289X
On the structure of abstract algebras, Proceedings Cambridge Phil. Soc, vol.31, pp.433-454, 1935. ,
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
Type Theory and Rewriting, 2001. ,
Term Graph Rewriting -syntax and semantics, 2001. ,
Term Rewriting and all That, 1998. ,
Uniqueness typing for functional languages with graph rewriting semantics, Mathematical Structures in Computer Science, vol.6, issue.6, pp.579-612, 1996. ,
Unification theory, Handbook of Automated Reasoning, volume I, chapter 8, pp.445-532, 2001. ,
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
Term graph rewriting, PARLE Parallel Architectures and Languages Europe, pp.141-158, 1987. ,
DOI : 10.1007/3-540-17945-3_8
(Cyclic) term graph rewriting is adequate for rational parallel term rewriting, 1997. ,
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
An algebraic presentation of term graphs via gsmonoidal categories, 1999. ,
Rewriting on cyclic structures: Equivalence of operational and categorical descriptions, Theoretical Informatics and Applications, pp.467-493, 1999. ,
A Formulation of the Simple Theory of Types, Journal of Symbolic Logic, vol.5, pp.56-68, 1941. ,
Calcul de réécriture : fondements et applications, Thèse de Doctorat d'Université, 2000. ,
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
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
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
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
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
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. ,
Fundamental properties of infinite trees, Theoretical Computer Science, vol.25, issue.2, pp.95-169, 1983. ,
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
Orderings for term-rewriting systems, Theoretical Computer Science, vol.17, pp.279-301, 1982. ,
An Overview of ASF+SDF, Language Prototyping, pp.1-31, 1996. ,
Unification via explicit substitutions: The case of higher-order patterns, Proceedings of JICSLP'96, 1996. ,
URL : https://hal.archives-ouvertes.fr/inria-00077203
Rewrite Systems, pp.244-320, 1990. ,
DOI : 10.1016/B978-0-444-88074-1.50011-1
Third order matching is decidable, Proceedings of LICS'92, 1992. ,
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. ,
RhomCal: an implementation of the explicit rewriting calculus Available on, 2005. ,
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
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
A gentle introduction to category theory ? the calculational approach, Lecture Notes of the STOP 1992 Summerschool on Constructive Algorithmics, pp.1-72, 1992. ,
Polymorphic rewriting conserves algebraic strong normalization and confluence, 16th Colloquium Automata, Languages and Programming, pp.137-150 ,
Generalized finitness of developments in typed lambda calculi, Journal of Automata, Languages and Combinatorics, vol.1, issue.4, pp.247-258, 1996. ,
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
The undecidability of the second order unification problem, Theoretical Computer Science, vol.13, pp.225-230, 1981. ,
A Comparison of RDF Query Languages, Proceedings of the Third International Semantic Web Conference, 2004. ,
DOI : 10.1007/978-3-540-30475-3_35
The Church-Rosser property and a result in combinatory logic, 1964. ,
Reductions of residuals are finite. Transactions of the, pp.345-361, 1978. ,
Implementing term rewriting by jungle evaluation, Theorique et Applications/Theoretical Informatics and Applications, 1991. ,
DOI : 10.1051/ita/1991250504451
Introduction to Combinators and Lambdacalculus, 1986. ,
A unification algorithm for typed lambda calculus, Theoretical Computer Science, vol.1, issue.1, pp.27-57, 1975. ,
Résolution d'equations dans les langages d'ordre 1, Thèse de Doctorat d'Etat, 1976. ,
Confluent reductions: Abstract properties and applications to term rewriting systems, Preliminary version in 18th Symposium on Foundations of Computer Science, pp.797-821, 1977. ,
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
Solving equations in abstract algebras: A rulebased survey of unification, Computational Logic: Essays in Honor of Alan Robinson, pp.257-321, 1991. ,
Abstract data type systems, Theoretical Computer Science, vol.173, issue.2, pp.349-391, 1997. ,
DOI : 10.1016/S0304-3975(96)00161-2
Natural semantics, 1987. ,
Algebraic graph derivations for graphical calculi, Proceedings of Graph- Theoretic Concepts in Computer Science, Cadenabbia (Como), Italy, pp.224-238, 1996. ,
Relational treatment of term graphs with bound variables, Journal of the IGPL, vol.6, issue.2, pp.259-303, 1998. ,
Simple Word Problems in Universal Algebras, Computational Problems in Abstract Algebra, pp.263-297, 1970. ,
DOI : 10.1007/978-3-642-81955-1_23
On 'on graph rewritings, Theoretical Computer Science, vol.52, issue.12, pp.37-58, 1987. ,
Expression reduction systems, Proceedings of I. Vekua Institute of Applied Mathematics, pp.200-220, 1990. ,
Rewriting, solving, proving. A preliminary version of a book available at www, 1999. ,
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
Transfinite reductions in orthogonal term rewriting systems, Proceedings 4th Conference on Rewriting Techniques and Applications, Como (Italy), 1991. also Report CS-R9041, CWI, 1990. ,
Attempts for generalizing the recursive path ordering, 1982. ,
Combinatory Reduction Systems, 1980. ,
Term Rewriting Systems, Handbook of Logic in Computer Science, 1990. ,
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
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
Combinatory reduction systems: introduction and survey, Theoretical Computer Science, vol.121, pp.279-308, 1993. ,
Interaction nets, POPL '90: Proceedings of the 17th ACM SIGPLAN- SIGACT symposium on Principles of programming languages, pp.95-108, 1990. ,
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. ,
Canonical algebraic simplifications, 1975. ,
A unification algorithm for abelian group theory, 1979. ,
Optimality and Concurrency in Interaction Systems, 1993. ,
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. ,
Réductions correctes et optimales dans le lambda-calcul, 1978. ,
The undecidability of ?-definability ,
Algebraic approach to single-pushout graph transformation, Theoretical Computer Science, vol.109, issue.12, pp.181-224, 1993. ,
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
The Polymorphic Rewriting-calculus [Type Checking v.s. Type Inference, Proc. of WRLA, 2004. ,
Description Abstraite des Systèmes de Réécriture, 1996. ,
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. ,
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
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
Resource description framework (RDF) ,
On theories with a combinatorial definition of equivalence, Annals of Math, pp.223-243, 1942. ,
Combining matching algorithms: The regular case, Journal of Symbolic Computation, vol.12, pp.633-653, 1991. ,
Orthogonal higher-order rewrite systems are confluent, Proceedings of the International Conference on Typed La mbda Calculi and Applications, pp.306-317, 1993. ,
Higher-order rewriting and equational reasoning, Automated Deduction ? A Basis for Applications. Volume I: Foundations. Kluwer, 1998. ,
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. ,
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. ,
Filtrage d'ordre supérieur, Thèse de Doctorat d'Université, 1996. ,
Des calculs de substitution explicites et de leur application a la compilation des langages fonctionnels, Thèse de Doctorat d'Université, 1997. ,
Internal labellings in lambda-calculus, Proceedings of Mathematical Foundations of Computer Science MFCS'90, pp.439-445, 1990. ,
?µ-calculus: An algorithmic interpretation of classical natural deduction, Proceedings of LPAR'92, pp.190-201, 1992. ,
Building in equational theories, Machine Intelligence, pp.73-90, 1972. ,
Handbook of Graph Grammars and Computing by Graph Transformation, pp.3-61, 1999. ,
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
Linear unification of higher-order patterns ,
Combining Decision Algorithms for Matching in the Union of Disjoint Equational Theories, Information and Computation, vol.126, issue.2, pp.144-160, 1996. ,
Tree-manipulating systems and Church-Rosser theorems, Journal of the ACM, vol.20, issue.1, pp.160-187, 1973. ,
Graph-grammars -an algebraic approach, IEEE Proceedings of the Fourteenth Annual Symposium on Switching and Automata Theory, pp.167-180, 1973. ,
Term graph rewriting: theory and practice, 1993. ,
Church-Rosser theorems for replacement systems, Algebra and Logic, Lectures Notes in Mathematics, vol.450, pp.291-307, 1975. ,
Completeness, invariance and lambda-definability, Journal Symbolic Logic, vol.47, issue.1, pp.17-26, 1982. ,
Computable numbers with an application to the entscheidungsproblem, Proc. London Math. Soc, vol.42, pp.230-65, 1937. ,
A new implementation technique for applicative languages. Software and Practice and Experience, pp.31-49, 1979. ,
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
A direct proof of the finite developments theorem, Journal Symbolic Logic, vol.50, issue.2, pp.339-343, 1985. ,
Klop counter example in the rho-calculus. Draft notes, 2003. ,
Calcul de réécriture : du typage à la déduction, Thèse de Doctorat d'Université, 2005. ,
Semantics and Pragmatics of the Lambda Calculus, 1971. ,
Rewriting, and equational unification: The higher-order cases ,
The Clausal Theory of Types, volume 21 of Cambridge Tracts in Theoretical Computer Science, 1993. ,