Rewriting Techniques and Applications: 20th International Conference, RTA 2009 Brasília, Brazil, June 29 - July 1, 2009 Proceedings

Description

This book constitutes the refereed proceedings of the 20th International Conference on Rewriting Techniques and Applications, RTA 2009, held in Brasília, Brazil, during June 29 - July 1, 2009. The 22 revised full papers and four system descriptions presented were carefully reviewed and selected from 59 initial submissions. The papers cover current research on all aspects of rewriting including typical areas of interest such as applications, foundational issues, frameworks, implementations, and semantics. Front Matter....Pages - Automatic Termination....Pages 1-16 Loops under Strategies....Pages 17-31 Proving Termination of Integer Term Rewriting....Pages 32-47 Dependency Pairs and Polynomial Path Orders....Pages 48-62 Unique Normalization for Shallow TRS....Pages 63-77 The Existential Fragment of the One-Step Parallel Rewriting Theory....Pages 78-92 Proving Confluence of Term Rewriting Systems Automatically....Pages 93-102 A Proof Theoretic Analysis of Intruder Theories....Pages 103-117 Flat and One-Variable Clauses for Single Blind Copying Protocols: The XOR Case....Pages 118-132 Protocol Security and Algebraic Properties: Decision Results for a Bounded Number of Sessions....Pages 133-147 YAPA: A Generic Tool for Computing Intruder Knowledge....Pages 148-163 Well-Definedness of Streams by Termination....Pages 164-178 Modularity of Convergence in Infinitary Rewriting....Pages 179-193 A Heterogeneous Pushout Approach to Term-Graph Transformation....Pages 194-208 An Explicit Framework for Interaction Nets....Pages 209-223 Dual Calculus with Inductive and Coinductive Types....Pages 224-238 Comparing Böhm-Like Trees....Pages 239-254 The Derivational Complexity Induced by the Dependency Pair Method....Pages 255-269 Local Termination....Pages 270-284 VMTL–A Modular Termination Laboratory....Pages 285-294 Tyrolean Termination Tool 2....Pages 295-304 From Outermost to Context-Sensitive Rewriting....Pages 305-319 A Fully Abstract Semantics for Constructor Systems....Pages 320-334 The $\Pi^0_2$ -Completeness of Most of the Properties of Rewriting Systems You Care About (and Productivity)....Pages 335-349 Unification in the Description Logic $\mathcal{EL}$ ....Pages 350-364 Unification with Singleton Tree Grammars....Pages 365-379 Unification and Narrowing in Maude 2.4....Pages 380-390 Back Matter....Pages -