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

WESTAPP 98

	ULTRA group Useful Logics, Types, Rewriting, and Applications		UKII UK Institute of Informatics, UK
	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:

New concepts in substitution calculi
Higher order types and explicit substitutions
Generalised techniques to show properties of substitution calculi
Relating explicit substitutions with other formalisms such as sequent calculi, linear logic, game semantics, etc.
Accommodating different reduction strategies and control operators
Use of explicit substitution in proof checking and proof search, in the implementation of programming languages and theorem provers
Different criteria useful to compare calculi with explicit substitutions
Applications of explicit substitutions to solve problems in other fields (e.g. higher order unification, set constraints etc.)

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.

IMPORTANT DATES

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.

INVITED SPEAKER

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

PROGRAM COMMITTEE

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)

LOCAL ORGANIZING COMMITTEE

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