WESTAPP 98

    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

             http://www.dcs.gla.ac.uk/~fairouz/call.html

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 fairouz@dcs.gla.ac.uk

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
de Paris, France).

PROGRAM COMMITTEE

 Roberto Di Cosmo    (Ecole Normale Superieure de Paris, France)
 Fairouz Kamareddine (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)