Termination or halting of computer processes was shown undecidable by Turing in the general case. However proof of termination plays a fundamental role in many applications, and challenges are theoretical as well as practical. In theoretical issues termination, especially termination of rewrite systems, is strongly connected to mathematical logic and proof theory and it inherits many concepts developed in established ordinal theory started by Cantor. However, termination of rewrite systems renews considerably the theory of ordinals, bringing new problems and new insights. In practical domains automated deduction systems integrate some tools for termination proofs, but usually they are rather poor. Towards wider use the development and integration of new, more friendly, more general and easier algorithms are required.
In May 1993, a workshop on termination was organised at St Andrews, where around forty researchers in the field met for the first time.
We are organising a second workshop which will take place in the mountain resort of La Bresse in les Vosges. We hope that this congenial location will offer the same friendly environment as at St Andrews and create the same fruitful exchanges. The scheduled date is just before the Rewriting Techniques and Applications conference (Kaiserslautern).
Topics: Here is a non limitative list of topics that could be presented at the workshop: well-quasi orders, Kruskal's theorem, recursive path order, lexicographic path order, multiset path order, length of derivation and orders, order hierarchies, ordinals and termination, proofs by interpretation, study of hard termination problems, design and implementation of new algorithms, integration in theorem provers and experiments, applications of termination.
People who wish to present a communication are invited to submit a one page abstract by January 2nd 1995 by e-mail at termination@loria.fr
Other Deadlines: Jan 30: program announcement, Mar 2: registration.
Francoise Bellegarde (U. de Franche-Comte, Besancon, France)
Adam Cichon (U. Henry Poincare, Nancy, France)
Isabelle Gnaedig (INRIA-Lorraine. Nancy, France)
Pierre Lescanne (CRIN-CNRS, Nancy, France)
Ursula Martin (U. St Andrews, Scotland)