Rewriting techniques and applications : 12th international conference, RTA 2001, Utrecht, the Netherlands, May | International Conference on Rewriting Techniques and Applications (12th : 2001 : Utrecht, Netherlands), Middeldorp, Aart, 1963-

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