[Prev][Next][Index][Thread]
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
records
- Proof synthesis and proof search via explicit substitutions
SUBMISSION
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.
PROGRAM COMMITTEE
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)
INVITED SPEAKERS
Jean-Jacques Levy (INRIA-Rocquencourt, France)
Per Martin-Lof (Stockholms University, Sweden)
IMPORTANT DATES
Submission: February 15,1999
Notification: March 30,1999
Final Version: May 15,1999
Workshop: July 5,1999
LOCAL ORGANIZING COMMITTEE
Andrea Asperti (University of Bologne, Italy)
Fausto Giunchiglia (University of Trento, Italy)