with variable bINding
DEADLINE: MONDAY 11 JUNE 2001
Siena, Italy, June 18, 2001, in
connection with IJCAR 2001
Topics | Registration
| Invited talk | Accepted
Papers | Schedule
| Program Committee | Important
Dates | Abstracts
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.
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
More specifically, contributions are solicited on all aspects
of mechanized reasoning about languages with variable binding, including,
but not limited to:
Case studies of metaprogramming, and the mechanization of the metatheory
of operational descriptions of programming languages and calculi. Papers
about the functional, imperative, object-oriented and concurrent methodologies
Case studies of the mechanization of the metatheory of abstract machines,
particularly machines for programming languages.
The theory of induction & recursion and coinduction & corecursion
on datatypes with variable binding.
Novel implementations of induction & recursion and coinduction &
corecursion on datatypes with variable binding, especially work related
to programming languages.
The theory and implementation of metalogical systems suitable for reasoning
about programming languages.
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.
Andrew Pitts, University
of Cambridge, has agreed to give an invited talk on
First Order Theory of Names and Binding
Andreas Abel (Carnegie Mellon, USA).
Representation of the Lambda-Mu-Calculus.
Gilles Dowek (INRIA, France), Therese Hardin (LIP6, UPMC, France) and Claude
Kirchner (LORIA & INRIA, France).
Theorem for an Extension of First-Order Logic with Binders.
Marino Miculan (Udine, Italy).
(Meta)Theory of Lambda-Calculus in the Theory of Contexts.
Dale Miller (Pennsylvania State, USA).
Christine Roeckl (LAMP-DI-EPFL, Switzerland).
Syntax for the Pi-Calculus in Isabelle/HOL using Permutations.
Carsten Schuermann, Dachuan Yu and Zhaozhong Ni (Yale, USA).
F_Omega in LF.
Rene Vestergaard (CNRS-IML, France) and James Brotherston (Edinburgh, UK).
Mechanisation of Barendregt-Style Equational Proofs (the Residual Perspective).
Simon J. Ambler, (University
Roy L. Crole,
(Chair, University of Leicester)
Amy Felty (University
Andrew Gordon (Microsoft
Furio Honsell (University
Tom Melham (University
Frank Pfenning (Carnegie Mellon
(reduced rates): Tuesday 15th May 2001.
(normal rates): Monday 1th June 2001.
Workshop date: Monday 18th June.
Call for Papers (obsolete)
Here you can find the call for papers in txt,
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
MERLIN 2001 is
supported by the Esprit
Working Group APPSEM.
Page maintained by Alberto Momigliano
Last modification: May, 31, 2001.
For more information : firstname.lastname@example.org.