workshop announcement

                         W E S T A P P'  9 9
       The Second International Workshop on Explicit Substitutions: 
             Theory and Applications to Programs and Proofs
                        CALL FOR PAPERS
                    July 5, 1999, Trento, Italy
                    FLoC'99 Affiliated Workshop 

         URL address: http://www.lri.fr/~kesner/westapp/call.html

Recently,  there has been growing  interest  in explicit substitutions as a
means of bridging the gap between theory and practice in the implementation
of   programming      languages,       theorem   provers      and     proof
checkers. Theoretically,    these  typically rely  on  calculi  that employ
substitution operations implicitly  at the meta-level; implementations  are
then   framed   in   terms  of  these     meta-level  operations.  Explicit
substitutions bring  the meta-level operations  down  into the object-level
calculus, where  they are represented  explicitly.  This  allows formal and
robust  models    to be   given  for  the   techniques  actually    used in
implementations, and  at the same time  allows more flexibility and control
on  unfinished  evaluations.  Explicit substitutions,   and more  generally
environment  machines, have recently proved to   be very useful in building
more efficient  programming languages and  proof assistants.  

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

- Use of explicit  substitution in implementation of programming languages,
  theorem provers and proof checkers
- Explicit substitutions calculi used for the design of abstract machines 
- New concepts in substitution calculi
- Generalised   techniques  to show  properties   of substitution calculi 
- Relating  explicit substitutions with  logic  formalisms such as  sequent
  calculi, linear logic, game semantics, etc.
- Accommodating different reduction strategies and control operators 
- Higher order types and explicit substitutions 
- Extensions of explicit substitution calculi to higher order formalisms
- 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.)
- Different  notions of  substitutions,   relations  with environments  and
- Proof synthesis and proof search via explicit substitutions


Authors are invited to submit an extended abstract up to 12 pages in length
excluding  references  and  appendices.  An   appendix containing  relevant
proofs is highly recommended.  Submission of abstracts in PostScript format
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 will select the best accepted papers of  the Journal Mathematical
Structures in Computer Science (MSCS). 

Email your full article in postscript format to Delia.Kesner@lri.fr. 

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


Luca    Cardelli            (Microsoft Research, UK)
Therese Hardin              (University Paris VI, France)
Fairouz Kamareddine         (University of Glasgow, UK)
Delia   Kesner (Organizer)  (Universite Paris-Sud, France) 
Shin-ya Nishizaki           (Tokyo Institute of Technology, Japan)
Valeria de Paiva            (University of Birmingham, UK)


Jean-Jacques Levy (INRIA-Rocquencourt, France)
Per Martin-Lof    (Stockholms University, Sweden) 


Submission:    February 15,1999
Notification:  March 30,1999
Final Version: May 15,1999
Workshop:      July 5,1999


Andrea Asperti     (University of Bologne, Italy)
Fausto Giunchiglia (University of Trento, Italy)