Rewrite-based Automated Reasoning: Challenges Ahead
Deepak Kapur (SUNY Albany)

Session: 10:00-10:30. Chair: Robert Nieuwenhuis.

Fine-grained Concurrent Completion
Claude Kirchner, Christopher Lynch & Christelle Scharff (INRIA Lorraine & CRIN)

Coffee Break: 10:30-11:00.

Session: 11:00-12:30. Chair: Ursula Martin.

AC-complete Unification and its Application to Theorem Proving
Alexandre Boudet, Evelyne Contejean & Claude Marché (Université de Paris-Sud & CNRS)

Superposition Theorem Proving for Abelian Groups Represented as Integer Modules
Jürgen Stuber (Max Planck Institut für Informatik)

Symideal Gröbner Bases
Manfred Göbel (Wilhelm-Schickard-Institut, Universität Tübingen)

Lunch Break: 12:30-14:00.

Session: 14:00-15:30. Chair: Nachum Dershowitz.

Termination of Constructor Systems
Thomas Arts (Utrecht University) & Jürgen Giesl (TH Darmstadt)

Dummy Elimination in Equational Rewriting
M.C.F. Ferreira (Utrecht University)

On Proving Termination by Innermost Termination
Bernhard Gramlich (Universität Kaiserslautern)

Coffee Break: 15:30-16:00.

Session: 16:00-17:30. Chair: Jürgen Avenhaus.

A Recursive Path Ordering for Higher-Order Terms in Eta-Long Beta-Normal Form
Jean-Pierre Jouannaud (CNRS & Université de Paris-Sud) & Albert Rubio (Universitat Politècnica de Catalunya)

Higher-Order Superposition for Dependent Types
Roberto Virga (Carnegie Mellon University)

Higher-Order Narrowing with Definitional Trees
Michael Hanus (RWTH Aachen) & Christian Prehofer (Technische Universität München)

Business Meeting: 20:00-21:30.

Design of a Proof Assistant
Gérard Huet (INRIA Rocquencourt)

Coffee Break: 10:30-11:00.

Session: 11:00-11:30. Chair: David Plaisted.

A Compiler for Nondeterministic Term Rewriting Systems
Marian Vittek (INRIA Lorraine, CRIN & ILOG Gentilly)

System Descriptions: 11:30-12:40. Chair: David Plaisted.

A New Proof Manager and Graphic Interface for the Larch Prover
Frédéric Voisin (CNRS & Université de Paris-Sud )

ReDuX 1.5: New Facets of Rewriting
Reinhard Bündgen, Carsten Sinz & Jochen Walter (Wilhelm-Schickard-Institut, Universität Tübingen)

CiME: Completion Modulo E*
Evelyne Contejean & Claude Marché (Université de Paris-Sud & CNRS)

Distributed Larch Prover (DLP): An Experiment in Parallelizing a Rewrite Rule-based Prover
Mark T. Vandevoorde (Massachusetts Institute of Technology) & Deepak Kapur (SUNY Albany)

EPIC: An Equational Programming Language - Abstract Machine and Supporting Tools
H.R. Walters & J.F.Th. Kamperman (CWI Amsterdam)

SPIKE-AC: a System for Proofs by Induction in Associative-Commutative Theories
Narjes Berregeb, Adel Bouhoula & Michaël Rusinowitch (INRIA Lorraine & CRIN)

On Gaining Efficiency in Completion-based Theorem Proving
Thomas Hillenbrand, Arnim Buch & Roland Fettig (Universität Kaiserslautern)

Lunch Break: 12:40-14:00.

System Demonstrations: 14:00-15:30.

Coffee Break: 15:30-16:00.

System Demonstrations: 16:00-18:00.

Combinatory Reduction Systems with Explicit Substitution that Preserve Strong Normalisation
Roel Bloo (University of Technology Eindhoven) & Kristoffer H. Rose (DIKU, University of Copenhagen)

Confluence Properties of Extensional and Non-Extensional Lambda-Calculi with Explicit Substitutions
Delia Kesner (CNRS & Université de Paris-Sud)

On the Power of Simple Diagrams
Roberto Di Cosmo (DMI-LIENS Paris)

Coffee Break: 10:30-11:00.

Session: 11:00-12:30. Chair: Friedrich Otto.

Coherence for Sharing Proof Nets
S. Guerrini (Università di Pisa), S. Martini (Università di Udine) & A. Masini (Università di Pisa)

Modularity of Termination in Term Graph Rewriting
M.R.K. Krishna Rao (Max Planck Institut für Informatik)

Confluence of Terminating Conditional Rewrite Systems Revisited
Bernhard Gramlich & Claus-Peter Wirth (Universität Kaiserslautern)

Lunch Break: 12:30-14:00.

Invited Lecture: 14:00-15:00. Chair: Paliath Narendran.

Applications of Rewrite Techniques in Monoids and Rings
Klaus Madlener (Universität Kaiserslautern)

Session: 15:00-15:30. Chair: Paliath Narendran.

Compositional Term Rewriting: An Algebraic Proof of Toyama's Theorem
Christoph Lüth (Universität Bremen)

Coffee Break: 15:30-16:00.

Session: 16:00-17:30. Chair: Hubert Comon.

The First-Order Theory of One-Step Rewriting is Undecidable
Ralf Treinen (Université de Paris-Sud)

An Algorithm for Distributive Unification
Manfred Schmidt-Schauß (J.W.-Goethe Universität Frankfurt)

On the Termination Problem for One-Rule Semi-Thue Systems
Géraud Sénizergues (LaBRI Talence)

Joint Banquet with LICS: 19:00-22:00. Chair: C.A. Gunter.
Dinner speech by Dana Scott on ``Some Reflections on Logic and Logicians''.

Efficient Second-Order Matching
Régis Curien (CRIN-CNRS & INRIA Lorraine), Zhenyu Qian & Hui Shi (Universität Bremen)

Linear Second-Order Unification
Jordi Levy (Universitat Politècnica de Catalunya)

Unification of Higher-Order Patterns in a Simply Typed Lambda-Calculus with Finite Products and Terminal Type
Roland Fettig & Bernd Löchner (Universität Kaiserslautern)

Coffee Break: 10:30-11:00.

Session: 11:00-13:00. Chair: Aart Middeldorp.

Deciding Strong Sequentiality for Orthogonal Term Rewriting Systems is in Co-NP
Irène Durand (LaBRI Talence)

Decidable Approximations of Term Rewriting Systems
Florent Jacquemard (CNRS & Université de Paris-Sud)

Semantics and Strong Sequentiality of Priority Term Rewriting Systems
Masahiko Sakai & Yoshihito Toyama (JAIST Ishikawa)

Higher-Order Families
Vincent van Oostrom (Technische Universität München)

FLoC Plenary Session: 20:00-21:30. Chair: M.Y. Vardi.

Calculi for Interactions
R. Milner (Cambridge University, United Kingdom)