Rewriting Techniques and Applications: 15th International Conference, RTA 2004, Aachen, Germany, June 3-5, 2004. Proceedings
Author: Vincent van Oostrom
Published by Springer Berlin Heidelberg
ISBN: 978-3-540-22153-1
DOI: 10.1007/b98160

Table of Contents:

Termination Analysis of the Untyped λ-Calculus
A Type-Based Termination Criterion for Dependently-Typed Higher-Order Rewrite Systems
Termination of S-Expression Rewriting Systems: Lexicographic Path Ordering for Higher-Order Terms
Monadic Second-Order Unification Is NP-Complete
A Certified AC Matching Algorithm
Matchbox: A Tool for Match-Bounded String Rewriting
TORPA: Termination of Rewriting Proved Automatically
Querying Unranked Trees with Stepwise Tree Automata
A Verification Technique Using Term Rewriting Systems and Abstract Interpretation
Rewriting for Fitch Style Natural Deductions
Efficient λ-Evaluation with Interaction Nets
Proving Properties of Term Rewrite Systems via Logic Programs
On the Modularity of Confluence in Infinitary Term Rewriting
mu-term: A Tool for Proving Termination of Context-Sensitive Rewriting
Automated Termination Proofs with AProVE
An Approximation Based Approach to Infinitary Lambda Calculi
Böhm-Like Trees for Term Rewriting Systems
Dependency Pairs Revisited
Inductive Theorems for Higher-Order Rewriting
The Joinability and Unification Problems for Confluent Semi-constructor TRSs

Includes bibliographical references and index
1. Termination analysis of the untyped [lambda]-calculus -- 2. A type-based termination of S-expression rewriting systems: lexicographic path ordering for higher-order terms -- 3. Monadic second-order unification is NP-complete -- 4. A certified AC matching algorithm -- 5. Matchbox: a tool for match-bounded string rewriting -- 6. TORPA: termination of rewriting proved automatically -- 7. Querying unranked trees with stepwise tree automata -- 8. A verification technique using term rewriting systems and abstract interpretation -- 9. Rewriting for fitch style natural deductions -- 10. Efficient [lambda]-evaluation with interaction nets -- 11. Proving properties of term rewrite systems via logic programs -- 12. On the modularity of confluence in infinitary term rewriting -- 13. MU-TERM: a tool for proving termination of context-sensitive rewriting -- 14. Automated termination proofs with AProVE -- 15. An approximation based approach to infinitary lambda calculli -- 16. Bohm-like trees for term rewriting systems -- 17. Dependency pairs revisited -- 18. Dependency pairs revisited -- 19. Inductive theorems for higher-order rewriting -- 20. The joinability and unification problems for confluent semi-constructor TRSs -- 21. A visual environment for developing context-sensitive term rewriting systems