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.