[Prev][Next][Index][Thread]

Workshop on Explicit Substitutions: Final call for papers

                         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 a nd CNRS).

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)