MERλIN 2005
ICFP 2005 Workshop on
MEchanized Reasoning about Languages with varIable biNding

Goals • Program committee • Invited talk • Important Dates • Accepted Papers • Call for Papers • Organizers • Steering committee • Proceedings • Workshop Programme • Past versions of the workshop • ICFP • Types Project

Goals of the Workshop

In the last decade or so, there has been a great deal of research in the development and use of computer-aided tools for reasoning formally about properties of programs and programming languages. Such work remains very active, with considerable progress and development completed, but much still to do. The broad aim of the proposed workshop is to run a short, but highly focussed meeting, which will provide researchers with a forum to review state-of-the-art results and techniques, to summarize current progress on key problems, and to evaluate the challenges we face over the next decade. We plan to provide a number of problems and challenges in advance of the workshop, and to solicit both position and solution papers, as well as regular submissions. This range of input will form the basis of a discussion forum which will form part of the workshop.

The broad subject areas of MERλIN 2005 are

More specifically, the syntax, static semantics and dynamic semantics of the calculus under study (object language) is represented within a meta-language such as the one of a (possibly interactive) theorem prover. The encodings may require the use of variable binding constructs, inductive/coinductive definitions and associated schemes of (co)recursion, as well as higher-order judgment schemata. It has been known for a long time that it is difficult to combine all these features in existing environments. New tools and methodologies have been proposed by many researchers making computer-aided formal reasoning in this field a reality. Indeed, such work has even led to the introduction of new programming languages based upon foundational work. Automating variable binding and associated properties can be difficult, but such automation pervades the encoding of semantics associated with modern and sophisticated languages. Our long term aim is to provide useful and convenient tools for the wider programming language community. Bringing interested researchers together for a day will benefit the experts, as well as young and new people. Contributions will be solicited on all aspects of mechanized reasoning about languages with variable binding, including, but not limited to:

MERλIN 2005 is a small Types workshop.

Program committee

Invited talk

Towards a Type Theory of Contexts

Frank Pfenning
Carnegie Mellon University, Pittsburgh, USA
[joint work with Brigitte Pientka and Aleks Nanevski]

At the 2003 Merlin workshop, we presented an initial report on providing a logical basis for the understanding of meta-variables. Our calculus rests on a contextual modality that is intrinsically connected to explicit substitutions, but does not provide a means for quantifying over substitutions or abstracting over contexts. In this talk we give a progress report on our attempts to obtain a modal type theory that integrates variables ranging over substitutions and contexts without losing its logical interpretation.

Important Dates

(*) Please notice that 29 July is also until when the block bookings and special rates from most of the local hotels are valid. All relevant info is available from http://www.cs.ioc.ee/tfp-icfp-gpce05/

Accepted Papers

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 merlin@dimi.uniud.it. If necessary, authors may submit three hard copies to Alberto Momigliano at postal address: Laboratory for Foundations of Computer Science, School of Informatics, The University of Edinburgh, Mayfield Road, Edinburgh EH9 3JZ, Scotland, UK.
As for any ACM sponsored workshop, the proceedings will appear in the ACM Digital Library.

Organizers

Steering committee

Roy L. Crole (University of Leicester, UK), Joëlle Despeyroux (INRIA, France), Furio Honsell (University of Udine, Italy), Dale Miller (INRIA, France), Tobias Nipkow (Technische Universität München, Germany), Randy Pollack (University of Edinburgh, UK).

Proceedings

Previous proceedings have appeared in Elsevier's Electronic Notes in Theoretical Computer Science and the ACM's Digital Library. In 2005 we plan to publish the proceedings in the digital library. Submitted papers will be subject to a regular peer review procedure which will require high standards. A preliminary proceeding volume containing the accepted papers will be distributed to the participants at the workshop. After that, authors of accepted papers will be asked to submit a revised version, taking into account feedback from the workshop.

Update: the electronic proceedings are available here.

Workshop Programme

9.00GPCE invited talk.
Session I
10.00Welcome by the PC and Workshop Chair
10:10Kevin Donnelly and Hongwei Xi
Combining higher-order abstract syntax with first-order abstract syntax in ATS
10.30Break
Session II
11.00Christian Urban and Michael Norrish
A formal treatment of the Barendregt variable convention in rule inductions
11.30James Cheney
Towards a general theory of names, binding and scope
12.00Marino Miculan, Ivan Scagnetto and Furio Honsell
Translating specifications from nominal logic to CIC with the theory of contexts
12.30Lunch break
Session III
14.30Frank Pfenning
Towards a type theory of contexts (invited talk)
15.30Aleksey Nogin, Alexei Kopylov, Xin Yu and Jason Hickey
A computational approach to reflective meta-reasoning about languages with bindings
16.00Break
Session IV
16.30Miki Tanaka and John Power
A unified category-theoretic formulation of typed binding signatures
17.00Olha Shkaravska
Types with semantics
17.30Panel Discussion (James Cheney, Bob Harper, Randy Pollack, Benjamin Pierce, Steve Zdancewic):
Beyond the POPLmark Challenge.

Past versions of the workshop

MERλIN 2001 was held in Siena, Italy, June 18, 2001, in connection with IJCAR 2001 (International Joint Conference on Automated Reasoning). It was organized by Roy L. Crole, Simon J. Ambler, and Alberto Momigliano (then at University of Leicester, UK).

MERλIN 2003 was held in Uppsala University, Sweden, August 26, 2003, and was associated with the federation meeting Principles, Logics and Implementations of high-level programming languages (PLI 2003), 25 to 29 August 2003. It was organized by Alberto Momigliano (then at University of Leicester, UK) and Marino Miculan (University of Udine, Italy).

Page maintained by Ivan Scagnetto. Last modified: Mon Aug 22 16:00:00 CET 2005