17. RTA 2006: Seattle, WA, USA

Frank Pfenning (Ed.): Term Rewriting and Applications, 17th International Conference, RTA 2006, Seattle, WA, USA, August 12-14, 2006, Proceedings. Lecture Notes in Computer Science 4098 Springer 2006, ISBN 3-540-36834-5 BibTeX

FLoC Plenary Talk

Randal E. Bryant:
Formal Verification of Infinite State Systems Using Boolean Methods. 1-3
Electronic Edition (link) BibTeX

Session 1. Constraints and Optimization

Michael Codish, Vitaly Lagoon, Peter J. Stuckey:
Solving Partial Order Constraints for LPO Termination. 4-18
Electronic Edition (link) BibTeX
Traian-Florin Serbanuta, Grigore Rosu:
Computationally Equivalent Elimination of Conditions. 19-34
Electronic Edition (link) BibTeX
Sergio Antoy, Daniel W. Brown, Su-Hui Chiang:
On the Correctness of Bubbling. 35-49
Electronic Edition (link) BibTeX
Joe Hendrix, Hitoshi Ohsaki, Mahesh Viswanathan:
Propositional Tree Automata. 50-65
Electronic Edition (link) BibTeX

Session 2. Equational Reasoning

Bernhard Gramlich, Salvador Lucas:
Generalizing Newman's Lemma for Left-Linear Rewrite Systems. 66-80
Electronic Edition (link) BibTeX
Piotr Hoffman:
Unions of Equational Monadic Theories. 81-95
Electronic Edition (link) BibTeX
Jean-Pierre Jouannaud:
Modular Church-Rosser Modulo. 96-107
Electronic Edition (link) BibTeX

Session 3. System Verification

Yannick Chevalier, Michaël Rusinowitch:
Hierarchical Combination of Intruder Theories. 108-122
Electronic Edition (link) BibTeX
Yohan Boichut, Thomas Genet:
Feasible Trace Reconstruction for Rewriting Approximations. 123-135
Electronic Edition (link) BibTeX

Invited Talk

Ahmed Bouajjani, Javier Esparza:
Rewriting Models of Boolean Programs. 136-150
Electronic Edition (link) BibTeX

Session 4. Lambda Calculus

Sylvain Salvati:
Syntactic Descriptions: A Type System for Solving Matching Equations in the Linear lambda-Calculus. 151-165
Electronic Edition (link) BibTeX
Yo Ohta, Masahito Hasegawa:
A Terminating and Confluent Linear Lambda Calculus. 166-180
Electronic Edition (link) BibTeX
Ariel Arbiser, Alexandre Miquel, Alejandro Ríos:
A Lambda-Calculus with Constructors. 181-196
Electronic Edition (link) BibTeX
José Espírito Santo, Maria João Frade, Luis Pinto:
Structural Proof Theory as Rewriting. 197-211
Electronic Edition (link) BibTeX

Session 5. Theorem Proving

Steven Obua:
Checking Conservativity of Overloaded Definitions in Higher-Order Logic. 212-226
Electronic Edition (link) BibTeX
Adam Koprowski:
Certified Higher-Order Recursive Path Ordering. 227-241
Electronic Edition (link) BibTeX
Takahito Aoto:
Dealing with Non-orientable Equations in Rewriting Induction. 242-256
Electronic Edition (link) BibTeX

Session 6. System Descriptions

Adam Koprowski:
TPA: Termination Proved Automatically. 257-266
Electronic Edition (link) BibTeX
Yuki Chiba, Takahito Aoto:
RAPT: A Program Transformation System Based on Term Rewriting. 267-276
Electronic Edition (link) BibTeX
Mathieu Turuani:
The CL-Atse Protocol Analyser. 277-286
Electronic Edition (link) BibTeX
Ian Wehrman, Aaron Stump, Edwin M. Westbrook:
Slothrop: Knuth-Bendix Completion with a Modern Termination Checker. 287-296
Electronic Edition (link) BibTeX

Invited Talk

Jürgen Giesl, Stephan Swiderski, Peter Schneider-Kamp, René Thiemann:
Automated Termination Analysis for Haskell: From Term Rewriting to Programming Languages. 297-312
Electronic Edition (link) BibTeX

Session 6. System Descriptions

Nao Hirokawa, Aart Middeldorp:
Predictive Labeling. 313-327
Electronic Edition (link) BibTeX
Dieter Hofbauer, Johannes Waldmann:
Termination of String Rewriting with Matrix Interpretations. 328-342
Electronic Edition (link) BibTeX
Yi Wang, Masahiko Sakai:
Decidability of Termination for Semi-constructor TRSs, Left-Linear Shallow TRSs and Related Systems. 343-356
Electronic Edition (link) BibTeX
Olivier Bournez, Florent Garnier:
Proving Positive Almost Sure Termination Under Strategies. 357-371
Electronic Edition (link) BibTeX

Session 8. Higher-Order Rewriting and Unification

Harrie Jan Sander Bruggink:
A Proof of Finite Family Developments for Higher-Order Rewriting Using a Prefix Property. 372-386
Electronic Edition (link) BibTeX
Jean-Pierre Jouannaud, Albert Rubio:
Higher-Order Orderings for Normal Rewriting. 387-399
Electronic Edition (link) BibTeX
Jordi Levy, Manfred Schmidt-Schauß, Mateu Villaret:
Bounded Second-Order Unification Is NP-Complete. 400-414
Electronic Edition (link) BibTeX