Aims and scope of the Workshop
Currently, there is considerable interest in the use of computer-aided
tools for reasoning formally about properties of programs and
programming languages. To this end, the syntax, static semantics and
dynamic semantics of the calculus under examination have to be
represented within a meta-language, such as the one of a (possibly
interactive) theorem prover. The encodings may need to address the use
of variable binding constructs, inductive/coinductive definitions and
associated schemata of recursion/corecursion, as well as higher-order judgment
schemata. Recently, new meta-logical tools and methodologies have
been proposed, making computer-aided formal reasoning in this field a
reality.
The broad aim of this workshop is to run a highly focussed meeting,
which will provide researchers and practitioners with a forum to
review state-of-the-art results and techniques, and to present recent
and new progress in:
- The automation of the (meta)theory of programming languages and
related calculi, particularly work which involves variable binding
and fresh name generation.
- The theoretical and practical issues concerning the encoding of
systems and languages with 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. Finally,
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
Contributions are solicited on all aspects of mechanized reasoning
about languages with variable and name 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 paradigms are welcomed.
- The theory and implementation 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 datatypes and programming languages with variable bindings.
- Description of working systems and tools.
Program Committee
Invited talk
Simon
Peyton-Jones (Microsoft Research, UK):
Scope, binding, and inlining in the Glasgow Haskell Compiler
Important Dates
- Submission: 16 June 2003
- Notification: 14 July 2003
- Final Version: 31 July 2003
- Workshop: 26 August 2003
Call for Papers
Three categories of papers are solicited:
- Category A: Detailed and technical accounts of new research: up
to fifteen pages including bibliography and appendices.
- Category B: Shorter accounts of work in progress and proposed
further directions, including discussion papers: up to ten pages
including bibliography and appendices.
- Category C: System descriptions presenting an implemented tool
and its novel features: up to five pages. A demonstration is
expected to accompany the presentation.
Papers of categories A and B must describe original, previously
unpublished work; simultaneous submission for publication in a journal
or a major conference must be clearly indicated. Papers must include
the postal address, an email address if possible, and telephone
number, for at least one contact author. Further, the category (either
A, B or C) must be noted. Authors are encouraged to use LaTeX; papers
should be submitted electronically as a PostScript or PDF file to the
email address merlin03@dimi.uniud.it. If
necessary, authors may submit three hard copies to Alberto Momigliano
at postal address: Department of Mathematics and Computer Science,
University of Leicester, University Road, Leicester, LE1 7RH, United
Kingdom.
As for any ACM sponsored workshop, the proceedings will
appear in the ACM Digital Library.
A detailed call for papers is available in many formats:
PDF,
PostScript,
DVI or
plain text.
Program of the workshop
The final program of the workshop,
with abstracts, is available.
Venue
MERλIN 2003 is associated with the federation meeting Principles, Logics and
Implementations of high-level programming languages (PLI 2003),
including the ACM SIGPLAN International Conference on
Principles and Practice of Declarative Programming (PPDP 2003) and
the ACM SIGPLAN International
Conference on Functional Programming (ICFP 2003), as well as associated
workshops. PLI'03 will run from 25 to 29 August 2003. The
meetings will take place at the Uppsala University.
The previous edition of MERλIN was colocated with IJCAR 2001, in Siena.
Pictures
Some pictures from the workshop are available.
Organizers
Organizers can be contacted at merlin03@dimi.uniud.it.
ACM SIGPLAN
Special Issue of Higher-Order and Symbolic Computation
The editors of Higher-Order and
Symbolic Computation have agreed to produce a special issue on the
topics of MERλIN. The special issue is open to all contributions, and
not only to papers presented at the workshop. Please send your paper,
as a PDF (preferred) or PS file, at the address merlin03@dimi.uniud.it, before
April 25, 2004. Please email us title, authors and a
short abstract in plain text before April 15, 2004.
A text-only version of this call for paper
is available.
Page maintained by Marino Miculan.
Last modified: Sun Mar 21 23:15:29 CET 2004
