MERLIN Call for Participation

[Roy L. Crole]

                       CALL FOR PARTICIPATION

                             Workshop on
                
     MEchanized Reasoning about Languages with variable bINding
                                     
                            (MERLIN 2001)  
                                     
    Siena, Italy, June 18-19, 2001 in connection with IJCAR 2001


                  **********************************
                  * http://www.mcs.le.ac.uk/merlin *
                  **********************************
              **** Early registration: May 15, 2001 ****
                  **********************************

Currently, there is considerable interest in the use of computers to
encode (operational) semantic descriptions of programming
languages. Such encodings are often done within the metalanguage of a
theorem prover or related system. The encodings may require the use of
variable binding constructs, inductive definitions, coinductive
definitions, and associated schemes of (co)recursion.

The aim of this workshop is to provide researchers with a forum to
review state of the art results and techniques, and to present recent
and new progress in the areas of:

  + The automation of the metatheory of programming languages,
particularly work which involves variable binding.

  + Theoretical and practical problems of encoding variable binding,
especially the representation of, and reasoning about, datatypes
defined from binding signatures.


IMPORTANT DATES

  Early registration:          **** May 15, 2001 ****
  MERLIN workshop:                 June 18, 2001
  IJCAR 2001:                   June 20-23, 2001


REGISTRATION

For details of registration, please see the IJCAR 2001 website at

  http://www.dii.unisi.it/~ijcar/


INVITED TALK

Andrew Pitts, University of Cambridge, has agreed to give an invited
talk on "A First Order Theory of Names and Binding".


ACCEPTED PAPERS

  Andreas Abel (Carnegie Mellon, USA).
    A Third-Order Encoding of the Lambda-Mu-Calculus.

  Gilles Dowek (INRIA, France), Therese Hardin (LIP6, UPMC, France)
  and Claude Kirchner (LORIA & INRIA, France).
    A Completeness Theorem for an Extension of First-Order Logic
    with Binders.

  Marino Miculan (Udine, Italy).
    Developing (Meta)Theory of Lambda-Calculus in the Theory of Contexts.

  Dale Miller (Pennsylvania State, USA).
    Encoding Generic Judgements.

  Christine Roeckl (LAMP-DI-EPFL, Switzerland).
    A First-Order Syntax for the Pi-Calculus in Isabelle/HOL using
    Permutations.

  Carsten Schurmann, Dachuan Yu and Zhaozhong Ni (Yale, USA).
    Case Study: Formal Development of Safe Intermediate Languages.

  Rene Vestergaard (CNRS-IML, France) and James Brotherston (Edinburgh, UK).
    The Mechanisation of Barendregt-Style Equational Proofs
    (the Residual Perspective).


PROGRAMME COMMITTEE
  
  Simon Ambler (University of Leicester)
  Roy Crole (Chair; University of Leicester) 
  Amy Felty (University of Ottawa)
  Andrew Gordon (Microsoft Research, Cambridge)
  Furio Honsell (University of Udine)
  Tom Melham (University of Glasgow)
  Frank Pfenning (Carnegie Mellon University)


FURTHER DETAILS

For further details about the Workshop, please contact one of

+  Roy L. Crole, email: R.Crole@mcs.le.ac.uk
+  Simon J. Ambler, email: S.Ambler@mcs.le.ac.uk
+  Alberto Momigliano (Local Organizer), email: A.Momigliano@mcs.le.ac.uk
 
at postal address:

Department of Mathematics and Computer Science,  
University of Leicester,  
University Road,  
LEICESTER,  
LE1 7RH,   
United Kingdom.