[Prev][Next][Index][Thread]
MERLIN Call for Participation
-
To: types@cis.upenn.edu, hvg@cl.cam.ac.uk, coq-club@pauillac.inria.fr, isabelle-users@cl.cam.ac.uk, info-hol@jaguar.cs.byu.edu, lego-club@dcs.ed.ac.uk, nuprlnotes@cs.cornell.edu, pvs@csl.sri.com, concurrency@cwi.nl, imps@linus.mitre.org, mizar-forum@mizar.uwb.edu.pl, softverf@nist.gov, rewriting@ens-lyon.fr, lprolog@cs.umn.edu, elf-list@cs.cmu.edu, lics@math.uic.edu, eacsl@dimi.uniud.it, eatcs-it@cs.unibo.it, formal-methods@cs.uidaho.edu, theorem-provers@ai.mit.edu, gulp@di.unipi.it, logic@cs.cornell.edu, theorynt@listserv.nodak.edu, ccp@sics.se, users@mozart-oz.org, compunode@dfki.de, announce@sigart.acm.org, CADEinc@cs.albany.edu, csl@dbai.tuwien.ac.at, linear@cs.stanford.edu, logic-list@cs.rice.edu, compulog-deduction@cs.bham.ac.uk, compulog@doc.imperial.ac.uk, deduktion@intellektik.informatik.th-darmstadt.de, qed@mcs.anl.gov, dreamers@dai.ed.ac.uk, lfcs-interest@dcs.ed.ac.uk, stp@dcs.gla.ac.uk, facs-members@lut.ac.uk, fme@mailbase.ac.uk, fm-info@air16.larc.nasa.gov, fsdm@cs.uq.oz.au, merlin@mcs.le.ac.uk, haskell@haskell.org, S.Ambler@mcs.le.ac.uk, R.Crole@mcs.le.ac.uk, am133@mcs.le.ac.uk, afelty@site.uottawa.ca, adg@microsoft.com, honsell@dimi.uniud.it, tfm@dcs.gla.ac.uk, fp@cs.cmu.edu, merlin@mcs.le.ac.uk, Andy Pitts <ap@cl.cam.ac.uk>, christine.roeckl@epfl.ch, abel@cs.cmu.edu, miculan@dimi.uniud.it, dale@cse.psu.edu, carsten@cs.yale.edu, vester@iml.univ-mrs.fr, dowek@icase.edu
-
Subject: MERLIN Call for Participation
-
From: "Roy L. Crole" <R.Crole@mcs.le.ac.uk>
-
Date: Fri, 04 May 2001 17:49:24 +0100
-
Sender: "Roy L. Crole" <rlc3@mcs.le.ac.uk>
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.