Rewriting Techniques and Applications: 12th International Conference, RTA 2001 Utrecht, The Netherlands, May 22–24, 2001 Proceedings

Henk Barendregt (auth.), Aart Middeldorp (eds.)9783540421177, 3540421173

This book constitutes the refereed proceedings of the 12th International Conference on Rewriting Techniques and Applications, RTA 2001, held in Utrecht, The Netherlands, in May 2001.
The 23 revised full papers presented together with two system descriptions were carefully reviewed and selected from 55 submissions. All current aspects of rewriting are addressed.

---

Table of contents :
Computing and Proving….Pages 1-1
Rewriting for Deduction and Verification….Pages 2-2
Universal Interaction Systems with Only Two Agents….Pages 3-14
General Recursion on Second Order Term Algebras….Pages 15-30
Beta Reduction Constraints….Pages 31-46
From Higher-Order to First-Order Rewriting….Pages 47-62
Combining Pattern E -Unification Algorithms….Pages 63-76
Matching Power….Pages 77-92
Dependency Pairs for Equational Rewriting….Pages 93-107
Termination Proofs by Context-Dependent Interpretations….Pages 108-121
Uniform Normalisation beyond Orthogonality….Pages 122-136
Verifying Orientability of Rewrite Rules Using the Knuth-Bendix Order….Pages 137-153
Relating Accumulative and Non-accumulative Functional Programs….Pages 154-168
Context Unification and Traversal Equations….Pages 169-184
Weakly Regular Relations and Applications….Pages 185-200
On the Parallel Complexity of Tree Automata….Pages 201-215
Transfinite Rewriting Semantics for Term Rewriting Systems….Pages 216-230
Goal-Directed E -Unification….Pages 231-245
The Unification Problem for Confluent Right-Ground Term Rewriting Systems….Pages 246-260
On Termination of Higher-Order Rewriting….Pages 261-275
Matching with Free Function Symbols — A Simple Extension of Matching?….Pages 276-290
Deriving Focused Calculi for Transitive Relations….Pages 291-305
A Formalised First-Order Con uence Proof for the λ-Calculus Using One-Sorted Variable Names (Barendregt Was Right after all … almost)….Pages 306-321
A Normal Form for Church-Rosser Language Systems….Pages 322-337
Confluence and Termination of Simply Typed Term Rewriting Systems….Pages 338-352
Parallel Evaluation of Interaction Nets with MPINE….Pages 353-356
Stratego: A Language for Program Transformation Based on Rewriting Strategies System Description of Stratego 0.5….Pages 357-361