Useful Logics, Types, Rewriting,
UK Institute of Informatics,
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:
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.|
Articles not obeying the page and date limit will not be considered.
|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)|