Rewriting Techniques and Applications: 12th International Conference, RTA 2001 Utrecht, The Netherlands, May 22–24, 2001 Proceedings
Author: Aart Middeldorp
Published by Springer Berlin Heidelberg
ISBN: 978-3-540-42117-7
DOI: 10.1007/3-540-45127-7

Table of Contents:

Computing and Proving
Rewriting for Deduction and Verification
Universal Interaction Systems with Only Two Agents
General Recursion on Second Order Term Algebras
Beta Reduction Constraints
From Higher-Order to First-Order Rewriting
Combining Pattern E-Unification Algorithms
Matching Power
Dependency Pairs for Equational Rewriting
Termination Proofs by Context-Dependent Interpretations
Uniform Normalisation beyond Orthogonality
Verifying Orientability of Rewrite Rules Using the Knuth-Bendix Order
Relating Accumulative and Non-accumulative Functional Programs
Context Unification and Traversal Equations
Weakly Regular Relations and Applications
On the Parallel Complexity of Tree Automata
Transfinite Rewriting Semantics for Term Rewriting Systems
Goal-Directed E-Unification
The Unification Problem for Confluent Right-Ground Term Rewriting Systems
On Termination of Higher-Order Rewriting

Includes bibliographical references and index
Computing and Proving / Henk Barendregt -- Rewriting for Deduction and Verification / Michael Rusinowitch -- Universal Interaction Systems with Only Two Agents / Denis Bechet -- General Recursion on Second Order Term Algebras / Alessandro Beraducci and Corrado Bohm -- Beta Reduction Constraints / Manuel Bodirsky, Katrin Erk and Alexander Koller / [et al.] -- From Higher-Order to First-Order Rewriting / Eduardo Bonelli, Delia Kesner and Alejandro Rios -- Combining Pattern E-Unification Algorithms / Alexandre Boudet and Evelyne Contejean -- Matching Power / Horatiu Cirstea, Claude Kirchner and Luigi Liquori -- Dependency Pairs for Equational Rewriting / Jurgen Giesl and Deepak Kapur -- Termination Proofs by Context-Dependent Interpretations / Dieter Hofbauer -- Uniform Normalisation beyond Orthogonality / Zurab Khasidashvili, Mizuhito Ogawa and Vincent van Oostrom -- Verifying Orientability of Rewrite Rules Using the Knuth-Bendix Order / Konstantin Korovin and Andrei Voronkov -- Relating Accumulative and Non-accumulative Functional Programs / Armin Kuhnemann, Robert Gluck and Kazuhiko Kakehi -- Context Unification and Traversal Equations / Jordi Levy and Mateu Villaret -- Weakly Regular Relations and Applications / Sebastien Limet, Pierre Rety and Helmut Seidl -- On the Parallel Complexity of Tree Automata / Markus Lohrey -- Transfinite Rewriting Semantics for Term Rewriting Systems / Salvador Lucas -- Goal-Directed E-Unification / Christopher Lynch and Barbara Morawska -- The Unification Problem for Confluent Right-Ground Term Rewriting Systems / Michio Oyamaguchi and Yoshikatsu Ohta -- On Termination of Higher-Order Rewriting / Femke van Raamsdonk -- Matching with Free Function Symbols -- A Simple Extension of Matching? / Christophe Ringeissen -- Deriving Focused Calculi for Transitive Relations / Georg Struth -- A Formalised First-Order Confluence Proof for the [lambda]-Calculus Using One-Sorted Variable Names (Barendregt Was Right after all ... almost) / Rene Vestergaard and James Brotherston -- A Normal Form for Church-Rosser Language Systems / Jens R. Woinowski -- Confluence and Termination of Simply Typed Term Rewriting Systems / Toshiyuki Yamada -- Parallel Evaluation of Interaction Nets with MPINE / Jorge Sousa Pinto -- Stratego: A Language for Program Transformation Based on Rewriting Strategies (System Description of Stratego 0.5) / Eelco Visser