Workshop on
MEchanized Reasoning about Languages with variable bINding
    (MERLIN 2001)


Siena, Italy, June 18, 2001, in connection with IJCAR 2001

Aims | Topics | Registration | Invited talk | Accepted Papers | Schedule | Program Committee | Important Dates | Abstracts | Organizers

Background and Aims

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 broad aims are to run a short, but highly focussed meeting, which will 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:

Advances in these areas may well have significance for a substantial part of the programming language community. Further, the long term goals of developing good and robust methods for program reasoning may find large scale application. Advances in the named research areas may well be beneficial in a very direct way. Automating variable binding and associated properties can be difficult, but such automation pervades the encoding of semantics associated with datatypes with binding. Techniques which simplify such work will prove very useful to the community. Further, bringing interested researchers together for a day will benefit those who have worked in the area for some time, as well as young and new people.


More specifically,  contributions are solicited on all aspects of mechanized reasoning about languages with variable binding, including, but not limited to:

Location and Registration

MERLIN'01 will be held in  Siena, Italy, June 18, 2001 in connection with  the International Joint Conference on Automated Reasoning (IJCAR).  For venue and suggested accommodation see the IJCAR 2001 web page. Please remember that participants must register with  IJCAR. REGISTRATIONS WILL BE ACCEPTED UNTIL JUNE 11 2001. After this date, registration must be made ON THE CONFERENCE SITE at the registration desk.

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 Representation 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 Judgments.
Christine Roeckl (LAMP-DI-EPFL, Switzerland).
A First-Order Syntax for the Pi-Calculus in Isabelle/HOL using Permutations.
Carsten Schuermann, Dachuan Yu and Zhaozhong Ni (Yale, USA).
Representing F_Omega in LF.
Rene Vestergaard (CNRS-IML, France) and James Brotherston (Edinburgh, UK).
The Mechanisation of Barendregt-Style Equational Proofs (the Residual Perspective).

Program Committee

Simon J. Ambler, (University of Leicester)
Roy L. 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)

Important Dates

Call for Papers (obsolete)

Here you can find the call for papers in txt, tex, ps and pdf format.


For further details about the Workshop, please contact one of

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

MERLIN 2001 is supported by the Esprit Working Group APPSEM.

Page maintained by Alberto Momigliano
Last modification: May, 31, 2001.
For more information :