The First International Workshop on Explicit Substitutions:

Theory and Applications to Programs and Proofs

March 29, 1998, Tsukuba, Japan

This workshop is organized in conjunction with RTA-98


ULTRA logo ULTRA group
Useful Logics, Types, Rewriting,
and Applications
UK Institute of Informatics,
The Engineering and Physical Sciences Research Council (EPSRC)

In the last few years, there has been an outburst of work on Explicit Substitutions (ES). ES attempt to bridge the gap between theory and implementation by internalising the computations required to evaluate substitutions within the calculus under study. This allows more flexibility and control on ordering work: propagating substitutions through a term can wait until the subterm is the focus of computation; a program can be halted without carrying out unnecessary computations; postponing unneeded work indefinitely (i.e. avoiding it completely); etc. Also, ES allow to formally model the techniques used in real implementations, like environment machines, and has recently proved to be quite useful in building more efficient proof assistants.

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

Extended abstracts (up to 8 pages excluding references and appendices) are invited (an appendix containing relevant proofs is highly recommended). Submission of abstracts in PostScript by e-mail is mandatory. Accepted abstracts will be collected into preliminary proceedings which will be available at the workshop. At least one author of each accepted abstract is expected to attend the workshop.

The PC may later on decide to select some of the accepted abstracts for a formal publication.

The workshop registration will be joint with RTA-98.


Submission deadline: December 3rd, 1997.
Notification of acceptance: February 1st, 1998.
Email your full article in postscript format to

Articles not obeying the page and date limit will not be considered.


There will be an invited talk by Pierre-Louis Curien (Ecole Normale Superieure and CNRS Paris).


Roberto Di Cosmo (Ecole Normale Superieure de Paris, France)
Fairouz Kamareddine (chair) (University of Glasgow, UK)
Delia Kesner (Universite d'Orsay, France)
Pierre Lescanne (Ecole Normale Superieure de Lyon, France)
Randy Pollack (BRICS, Aarhus, Denmark)


Aart Middeldorp (University of Tsukuba, Japan)
Tetsuo Ida (University of Tsukuba, Japan)