WESTAPP 2000

[Czeslaw Bylinski <bylinski@math.uwb.edu.pl>]

---------- Forwarded message ----------
Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39])
	by mizar.uwb.edu.pl (8.9.3/8.9.3) with ESMTP id PAA06790
	for <mizar-forum@mizar.uwb.edu.pl>; Mon, 7 Feb 2000 15:01:07 +0100 (MET)
Date: Mon, 7 Feb 2000 15:02:09 +0100 (MET)
Message-Id: <200002071402.PAA32249@couchey.inria.fr>
X-Authentication-Warning: couchey.inria.fr: hardin set sender to hardin@couchey.inria.fr using -f
From: Therese Hardin <hardin@couchey.inria.fr>
To: acl2@lists.cc.utexas.edu, bra-types@cs.chalmers.se, categories@mta.ca,
        colt@cs.uiuc.edu, concurrency@cwi.nl, coq-club@pauillac.inria.fr,
        elf-list@cs.cmu.edu, facs-members@lut.ac.uk, facs@lboro.ac.uk,
        formal-methods@cs.uidaho.edu, forum@jsoftware.com, fsdm@it.uq.edu.au,
        IFIP-WG1_3-Members@brics.dk, imps@linus.mitre.org,
        info-hol@leopard.cs.byu.edu, isabelle-users@cl.cam.ac.uk,
        isss-people@ics.uci.edu, lambda-usergroup@dcs.ed.ac.uk,
        lego-club@dcs.ed.ac.uk, lics@research.bell-labs.com,
        logic-list@cs.rice.edu, logic@cs.stanford.edu,
        logic@theory.lcs.mit.edu, lotos-na@site.uottawa.ca,
        lprolog-list@cis.upenn.edu, lprolog@cis.upenn.edu,
        mizar-forum@mizar.uwb.edu.pl, nuprlnotes@cs.cornell.edu,
        papm@dcs.ed.ac.uk, pvs@csl.sri.com, qed@mcs.anl.gov,
        rewriting@ens-lyon.fr, softverf@nist.gov, tfm-list@doc.ic.ac.uk,
        theorem-provers@ai.mit.edu, zforum@prg.ox.ac.uk, fairouz@dcs.gla.ac.uk,
        fairouz@dcs.gla.ac.uk, hardin@spi.lip6.fr, Gilles.Dowek@inria.fr,
        debruijn@win.tue.nl, gopalan@cs.uchicago.edu, catarina@cs.chalmers.se,
        jbw@cee.hw.ac.uk
Subject: WESTAPP2000

     [We apologize if you receive multiple copies of this message] 

              WESTAPP'2000:  CALL FOR PAPERS

 The Third International Workshop on Explicit Substitutions:
        Theory and Applications to Programs and Proofs
     RTA'2000 Affiliated Workshop, July 13, 2000, Norwich, U. K.

             http://www.sys.uea.ac.uk/RTA2000, 
             http://www.lip6.fr/~hardin/westapp/call.html



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.)
- 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.

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.

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 University of Technology,
                        The Netherlands)
Gopalan Nadathur       (Loyola University of Chicago, US)

IMPORTANT DATES

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