12. RTA 2001: Utrecht, The Netherlands

Invited Talks

• Henk Barendregt:
  Computing and Proving. 1
  
• Michaël Rusinowitch:
  Rewriting for Deduction and Verification. 2
  

Regular Papers

• Denis Béchet:
  Universal Interaction Systems with Only Two Agents. 3-14
  
• Alessandro Berarducci, Corrado Böhm:
  General Recursion on Second Order Term Algebras. 15-30
  
• Manuel Bodirsky, Katrin Erk, Alexander Koller, Joachim Niehren:
  Beta Reduction Constraints. 31-46
  
• Eduardo Bonelli, Delia Kesner, Alejandro Ríos:
  From Higher-Order to First-Order Rewriting. 47-62
  
• Alexandre Boudet, Evelyne Contejean:
  Combining Pattern E-Unification Algorithms. 63-76
  
• Horatiu Cirstea, Claude Kirchner, Luigi Liquori:
  Matching Power. 77-92
  
• Jürgen Giesl, Deepak Kapur:
  Dependency Pairs for Equational Rewriting. 93-108
  
• Dieter Hofbauer:
  Termination Proofs by Context-Dependent Interpretations. 108-121
  
• Zurab Khasidashvili, Mizuhito Ogawa, Vincent van Oostrom:
  Uniform Normalisation beyond Orthogonality. 122-136
  
• Konstantin Korovin, Andrei Voronkov:
  Verifying Orientability of Rewrite Rules Using the Knuth-Bendix Order. 137-153
  
• Armin Kühnemann, Robert Glück, Kazuhiko Kakehi:
  Relating Accumulative and Non-accumulative Functional Programs. 154-168
  
• Jordi Levy, Mateu Villaret:
  Context Unification and Traversal Equations. 169-184
  
• Sébastien Limet, Pierre Réty, Helmut Seidl:
  Weakly Regular Relations and Applications. 185-200
  
• Markus Lohrey:
  On the Parallel Complexity of Tree Automata. 201-215
  
• Salvador Lucas:
  Transfinite Rewriting Semantics for Term Rewriting Systems. 216-230
  
• Christopher Lynch, Barbara Morawska:
  Goal-Directed E-Unification. 231-245
  
• Michio Oyamaguchi, Yoshikatsu Ohta:
  The Unification Problem for Confluent Right-Ground Term Rewriting Systems. 246-260
  
• Femke van Raamsdonk:
  On Termination of Higher-Order Rewriting. 261-275
  
• Christophe Ringeissen:
  Matching with Free Function Symbols - A Simple Extension of Matching? 276-290
  
• Georg Struth:
  Deriving Focused Calculi for Transitive Relations. 291-305
  
• René Vestergaard, James Brotherston:
  A Formalised First-Order Confluence Proof for the lambda-Calculus Using One-Sorted Variable Names. 306-321
  
• Jens R. Woinowski:
  A Normal Form for Church-Rosser Language Systems. 322-337
  
• Toshiyuki Yamada:
  Confluence and Termination of Simply Typed Term Rewriting Systems. 338-352
  

System Descriptions

• Jorge Sousa Pinto:
  Parallel Evaluation of Interaction Nets with MPINE. 353-356
  
• Eelco Visser:
  Stratego: A Language for Program Transformation Based on Rewriting Strategies. 357-362