Accepted Papers

Adam Koprowski
Certified Higher-Order Recursive Path Ordering

Takahito Aoto
Dealing with Non-Orientable Equations in Rewriting Induction

Piotr Hoffman
Unions of Equational Monadic Theories

Yuki Chiba, Takahito Aoto
RAPT: A Program Transformation System based on Term Rewriting

Harrie Jan Sander Bruggink
A Proof of Finite Family Developments for Higher-Order Rewriting using a Prefix Property

Steven Obua
Checking Conservativity of Overloaded Definitions in Higher-Order Logic

Nao Hirokawa, Aart Middeldorp
Predictive Labeling

Jean-Pierre Jouannaud, Albert Rubio
Higher-Order Orderings for Normal Rewriting

Michael Codish, Vitaly Lagoon, and Peter Stuckey
Solving Partial Order Constraints for LPO Termination

Yannick Chevalier, Michael Rusinowitch
Hierarchical Combination of Intruder Theories

Yi Wang, Masahiko Sakai
Decidability of Termination for Semi-Constructor TRSs, Left-Linear Shallow TRSs and Related Systems

Yohan Boichut, Thomas Genet
Feasible Trace Reconstruction for Rewriting Approximations

Jean-Pierre Jouannaud
Modular Church-Rosser Modulo

Dieter Hofbauer, Johannes Waldmann
Termination of String Rewriting with Matrix Interpretations

Sergio Antoy, Daniel Brown, and Su-Hui Chiang
On the Correctness of Bubbling

Jose Espirito Santo, Maria João Frade, and Luís Pinto
Structural Proof Theory as Rewriting

Yo Ohta, Masahito Hasegawa
A Terminating and Confluent Linear Lambda Calculus

Mathieu Turuani
The CL-Atse Protocol Analyser

Adam Koprowski
TPA: Termination Proved Automatically

Ian Wehrman, Aaron Stump, and Edwin Westbrook
Slothrop: Knuth-Bendix Completion with a Modern Termination Checker

Bernhard Gramlich, Salvador Lucas
Generalizing Newman's Lemma for Left-Linear Rewrite Systems

Jordi Levy, Manfred Schmidt-Schauss, and Mateu Villaret
Bounded Second-Order Unification is NP-Complete

Joe Hendrix, Hitoshi Ohsaki, and Mahesh Viswanathan
Propositional Tree Automata

Olivier Bournez, Florent Garnier
Proving Positive Almost Sure Termination Under Strategies

Traian Serbanuta, Grigore Rosu
Computationally Equivalent Elimination of Conditions

Ariel Arbiser, Alexandre Miquel, and Alejandro Ríos
A Lambda-Calculus with Constructors

Sylvain Salvati
Syntactic Descriptions: a Type System for Solving Matching Equations in the Linear Lambda-Calculus