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.)
This workshop delves into all aspects of termination of processes. Though, the halting of computer programs, for example, is undecidable, methods of establishing termination play a fundamental role in many applications and the challenges are both practical and theoretical. From a practical point of view, proving termination is a central problem in software development and formal methods for termination analysis are essential for program verification. From a theoretical point of view, termination is central in mathematical logic and ordinal theory.
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.