MERλIN 2003
Second ACM SIGPLAN Workshop on
MEchanized Reasoning about Languages with varIable biNding

Aims • Topics • Program Committee • Invited talk • Important Dates • Call for Papers • Program • Venue • Organizers • Sponsors • Pictures • HOSC Special Issue

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:

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.


Contributions are solicited on all aspects of mechanized reasoning about languages with variable and name binding, including, but not limited to:

Program Committee

Invited talk

Simon Peyton-Jones (Microsoft Research, UK): Scope, binding, and inlining in the Glasgow Haskell Compiler

Important Dates

Call for Papers

Three categories of papers are solicited: 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 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.


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 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, 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