Rewriting Techniques and Applications

Session 1
- Solved Forms for Path Ordering Constraints
- Jeopardy
- Strategic Pattern Matching

Session 2:
- On the Strong Normalization of Natural Deduction with Permutation-Conversions
- Normalisation in Weakly Orthogonal Rewriting
- Strong Normalization of Proof Nets Modulo Structural Congruences

Session 3: Invited Talk
- Hierarchical Graph Decompositions Defined by Grammars and Logical Formulas

Session 4:
- Undecidability of the Part of the Theory of Ground Term Algebra Modulo an AC Symbol
- Deciding the Satisfiability of Quantifier Free Formulae on One-Step Rewriting
- A New Result about the Decidability of the Existential One-Step Rewriting Theory

Session 5:
- A Fully Syntactic AC-RPO
- Theory Path Orderings
- A Characterisation of Multiply Recursive Functions with Higman's Lemma

Session 6:
- Deciding the Word Problem in the Union of Equational Theories Sharing Constructors
- Normalization via Rewrite Closures
- Test Sets for the Universal and Existential Closure of Regular Tree Languages

Session 7: Invited Tutorial
- Higher-Order Rewriting

Session 8: System Descriptions
- The Maude System
- TOY: A Multiparadigm Declarative System
- UniMoK: A System for Combining Equational Unification Algorithms
- : A Laboratory for Rapid Term Graph Rewriting

Session 9:
- Decidability for Left-Linear Growing Term Rewriting Systems
- Transforming Context-Sensitive Rewrite Systems
- Context-Sensitive AC-rewriting

Session 10:
- The Calculus of Algebraic Constructions
- HOL-??: An Intentional First-Order Expression of Higher-Order Logic

Session 11: Invited Talk
- On the Connections between Rewriting and Formal Language Theory

Session 12:
- A Rewrite System Associated with Quadratic Pisot Units
- Fast Rewriting of Symmetric Polynomials
- On Implementation of Tree Synchronized Languages