WESTAPP 2001 | May 20 |

5^{th} International Workshop on Termination |
May 20-21 |

IFIP Working Group 1.6 on Term Rewriting | May 25 |

Reduction Strategies in Rewriting and Programming | May 26 |

Recently, there has been growing interest in explicit substitutions as a means of bridging the gap between theory and practice in the implementation of programming languages, theorem provers and proof checkers. Theoretically, these typically rely on calculi that employ substitution operations implicitly at the meta-level; implementations are then framed in terms of these meta-level operations. Explicit substitutions bring the meta-level operations down into the object-level calculus, where they are represented explicitly. This allows formal and robust models to be given for the techniques actually used in implementations, and at the same time allows more flexibility and control on unfinished evaluations. Explicit substitutions, and more generally environment machines, have recently proved to be very useful in building more efficient programming languages and proof assistants.

The aim of this workshop is to bring together researchers working on both theoretical and applied aspects of explicit substitutions, to present recent work (possibly still in progress), and to discuss new ideas and emerging trends in topics including the following:

- Use of explicit substitution in implementation of programming languages, theorem provers and proof checkers
- Explicit substitutions calculi and abstract machines
- Accommodating different reduction strategies and control operators
- Different notions of substitutions, relations with environments and records
- Types and explicit substitutions
- Extensions of explicit substitution calculi to higher order formalisms
- New concepts in substitution calculi
- New techniques to show properties of substitution calculi
- Comparison of calculi of explicit substitution
- Relating explicit substitutions with logic formalisms (sequents, linear logic, game semantics, etc.)
- Proof synthesis and proof search via explicit substitutions
- Applications of explicit substitutions to other fields (e.g. higher order rewriting, higher order unification, set constraints etc.)

Visit the local WESTAPP site on http://www.ens-lyon.fr/~plescann/WESTAPP01/call/call.html

Visit the local WST site on http://www.cs.tau.ac.il/~nachumd/wst01.html

- Rewriting for computing and reasoning
- Theoretical studies of the rewriting relation of different orders.
- Complexity issues of rewriting.
- Compilation techniques and applications.
- Theory and applications of rewriting logic and calculus
- Application of rewriting to constraint solving, theorem proving and algebraic specifications
- The design, promotion and teaching of rewrite based techniques and applications.

Visit the local IFIP site on http://rewriting.loria.fr/IFIP-WG1.6/

The need for a deeper understanding of reduction strategies in rewriting and programming, both in theory and practice, is obvious, since they bridge the gap between unrestricted general rewriting (computation) and (more deterministic) rewriting with particular strategies (programming). Moreover, reduction strategies provide a natural way to go from operational principles (e.g., graph and term rewriting, narrowing, lambda-calculus) and semantics (e.g., normalization, computation of values, infinitary normalization, head-normalization) to implementations of programming languages.

Visit the local WRS site on http://www.logic.at/wrs01/