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 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.
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.
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.
The final program of the workshop, with abstracts, is available.
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.
Some pictures from the workshop are available.
Organizers can be contacted at merlin03@dimi.uniud.it.
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.