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

WESTAPP - 2nd Call for Papers

                     RTA'2000 Affiliated Workshop

	       NEW SUBMISSION DEADLINE: MARCH 26, 2000
		      (previously March 12, 2000)
                      
                       July 13, 2000, Norwich, U. K.

                  http://www.sys.uea.ac.uk/RTA2000 
                   http://www.lip6.fr/westapp2000

PROGRAM COMMITTEE

Catarina Coquand   (Chalmers U. and U. of Goteborg,Sweden)
Gilles Dowek       (INRIA Rocquencourt, France)
Therese Hardin(Organizer)   (U. Paris VI and INRIA Rocq., France)
Gopalan Nadathur   (Loyola U. of Chicago, US)
Joe Wells         (Heriot-Watt U., UK)


INVITED SPEAKERS

Prof. N. G.  de Bruijn (Eindhoven U. of Technology,The Netherlands)
Gopalan Nadathur       (Loyola University of Chicago, US)

SCOPE OF THE WORKSHOP

Explicit substitutions are 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:
 

- Properties of substitution calculi (normalization, confluence,
     strategies, etc.)

-  Relating explicit substitutions with logical formalisms 
     (sequent calculi, linear logic, game semantics, higher-order 
     logic, type theories, etc.)

-  Relating explicit substitutions with programming concepts 
     (environments, records, etc.).

- Theorem provers and proof checkers based on explicit 
     substitutions.

-  Design of abstract machines and implementations of programming
     languages based on explicit substitution.

-  Extensions of explicit substitution calculi.


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.

 Email your full article in postscript format to
 Therese.Hardin@inria.fr


IMPORTANT DATES

Submission:   March 26, 2000
Notification:  May 14,2000
Final Version:  June 2, 2000
Workshop:  July 13
RTA:   July 10-12,2000