Workshop on
MEchanized
Reasoning
about
Languages
with variable bINding
(MERLIN 2001)
REGISTRATION
DEADLINE: MONDAY 11 JUNE 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:
-
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.
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.
Topics
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
are welcomed.
-
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.
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
-
Early registration
(reduced rates): Tuesday 15th May 2001.
-
Registration
(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,
tex,
ps
and pdf format.
Organizers
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 : merlin@mcs.le.ac.uk.