Term Rewriting and Applications : 17th International Conference, RTA 2006 Seattle, WA, USA, August 12-14, 2006 Proceedings

by Pfenning, Frank

• ISBN13: 9783540368342
• ISBN10: 3540368345
• Format: Paperback
• Copyright: 2006-09-15
• Publisher: Springer Verlag

Summary

This book constitutes the refereed proceedings of the 17th International Conference on Rewriting Techniques and Applications, RTA 2006, held in Seattle, WA, USA in August 2006 within the scope of FLoC 2006, the 2006 Federated Logic Conference. The 23 revised full papers and 4 systems description papers carefully reviewed and selected from 52 initial submissions are presented together with 2 invited talks and a plenary talk of the hosting FLoC conference. The papers are organized in topical sections on constraints and optimization, equational reasoning, system verification, lambda calculus, theorem proving, system descriptions, termination, and higher-order rewriting and unification.

Table of Contents

FLoC Plenary Talk
Formal Verification of Infinite State Systems Using Boolean Methods	p. 1
Constraints and Optimization
Solving Partial Order Constraints for LPO Termination	p. 4
Computationally Equivalent Elimination of Conditions	p. 19
On the Correctness of Bubbling	p. 35
Propositional Tree Automata	p. 50
Equational Reasoning
Generalizing Newman's Lemma for Left-Linear Rewrite Systems	p. 66
Unions of Equational Monadic Theories	p. 81
Modular Church-Rosser Modulo	p. 96
System Verification
Hierarchical Combination of Intruder Theories	p. 108
Feasible Trace Reconstruction for Rewriting Approximations	p. 123
Invited Talk
Javier Esparza: Rewriting Models of Boolean Programs	p. 136
Lambda Calculus
Syntactic Descriptions: A Type System for Solving Matching Equations in the Linear [Lambda]-Calculus	p. 151
A Terminating and Confluent Linear Lambda Calculus	p. 166
A Lambda-Calculus with Constructors	p. 181
Structural Proof Theory as Rewriting	p. 197
Theorem Proving
Checking Conservativity of Overloaded Definitions in Higher-Order Logic	p. 212
Certified Higher-Order Recursive Path Ordering	p. 227
Dealing with Non-orientable Equations in Rewriting Induction	p. 242
System Descriptions
TPA: Termination Proved Automatically	p. 257
RAPT: A Program Transformation System Based on Term Rewriting	p. 267
The CL-Atse Protocol Analyser	p. 277
Slothrop: Knuth-Bendix Completion with a Modern Termination Checker	p. 287
Invited Talk
Jurgen Giesl: Automated Termination Analysis for Haskell: From Term Rewriting to Programming Languages	p. 297
Termination
Predictive Labeling	p. 313
Termination of String Rewriting with Matrix Interpretations	p. 328
Decidability of Termination for Semi-constructor TRSs, Left-Linear Shallow TRSs and Related Systems	p. 343
Proving Positive Almost Sure Termination Under Strategies	p. 357
Higher-Order Rewriting and Unification
A Proof of Finite Family Developments for Higher-Order Rewriting Using a Prefix Property	p. 372
Higher-Order Orderings for Normal Rewriting	p. 387
Bounded Second-Order Unification Is NP-Complete	p. 400
Author Index	p. 415
Table of Contents provided by Ingram. All Rights Reserved.