W E S T A P P' 9 9 The Second International Workshop on Explicit Substitutions: Theory and Applications to Programs and Proofs SECOND 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 (Heriot-Watt University, UK) Delia Kesner (PC Chair) (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 RTA & LICS: July 2-5, 1999 CADE & CAV: July 7-10, 1999 LOCAL ORGANIZING COMMITTEE Andrea Asperti (University of Bologne, Italy) Fausto Giunchiglia (University of Trento, Italy)