María Alpuente, Santiago Escobar, José Iborra (auth.), Andrei Voronkov (eds.)3540705880, 9783540705888
This book constitutes the refereed proceedings of the 19th International Conference on Rewriting Techniques and Applications, RTA 2008, held in Hagenberg, Austria, July 15-17, in June 2008 as part of the RISC Summer 2008.
The 30 revised full papers presented were carefully reviewed and selected from 57 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.
Table of contents :
Front Matter….Pages –
Modular Termination of Basic Narrowing….Pages 1-16
Linear-algebraic λ -calculus: higher-order, encodings, and confluence…..Pages 17-31
Term-Graph Rewriting Via Explicit Paths….Pages 32-47
Finer Is Better: Abstraction Refinement for Rewriting Approximations….Pages 48-62
A Needed Rewriting Strategy for Data-Structures with Pointers….Pages 63-78
Effectively Checking the Finite Variant Property….Pages 79-93
Dependency Pairs for Rewriting with Built-In Numbers and Semantic Data Structures….Pages 94-109
Maximal Termination….Pages 110-125
Usable Rules for Context-Sensitive Rewrite Systems….Pages 126-141
Combining Equational Tree Automata over AC and ACI Theories….Pages 142-156
Closure of Hedge-Automata Languages by Hedge Rewriting….Pages 157-171
On Normalisation of Infinitary Combinatory Reduction Systems….Pages 172-186
Innermost Reachability and Context Sensitive Reachability Properties Are Decidable for Linear Right-Shallow Term Rewriting Systems….Pages 187-201
Arctic Termination …Below Zero….Pages 202-216
Logics and Automata for Totally Ordered Trees….Pages 217-231
Diagram Rewriting for Orthogonal Matrices: A Study of Critical Peaks….Pages 232-245
Nominal Unification from a Higher-Order Perspective….Pages 246-260
Functional-Logic Graph Parser Combinators….Pages 261-275
Proving Quadratic Derivational Complexities Using Context Dependent Interpretations….Pages 276-290
Tree Automata for Non-linear Arithmetic….Pages 291-305
Confluence by Decreasing Diagrams….Pages 306-320
A Finite Simulation Method in a Non-deterministic Call-by-Need Lambda-Calculus with Letrec, Constructors, and Case….Pages 321-335
Root-Labeling….Pages 336-350
Combining Rewriting with Noetherian Induction to Reason on Non-orientable Equalities….Pages 351-365
Deciding Innermost Loops….Pages 366-380
Termination Proof of S-Expression Rewriting Systems with Recursive Path Relations….Pages 381-391
Encoding the Pure Lambda Calculus into Hierarchical Graph Rewriting….Pages 392-408
Revisiting Cut-Elimination: One Difficult Proof Is Really a Proof….Pages 409-424
Reduction Under Substitution….Pages 425-440
Normalization of Infinite Terms….Pages 441-455
Back Matter….Pages –
Reviews
There are no reviews yet.