Call for Papers
                          
                         Third ACM Workshop
                
MEchanized Reasoning about Languages with variable bInding and Names
                                     
                            (MERLIN 2005)  
                                     
                       Affiliated with ICFP'05 
                  Tallinn, Estonia, 30 September 2005

                  **********************************
                  * http://merlin.dimi.uniud.it/   *
                  **********************************

KEYWORDS 

Induction and Coinduction, Logical Frameworks, Mechanization, 
Metaprogramming, Operational Semantics, Programming Languages, 
Theorem Proving, Variable Binding.

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 are providing a number of problems and challenges related 
to the workshop topics and we solicit both position and solution papers.  
We hope this will contribute to  a discussion which will be an integral 
part of the workshop. A preliminary collection of problems and challenges 
is available at http://homepages.inf.ed.ac.uk/amomigl1/maincha.html.

The broad subject areas of MERLIN 2005 are
+ 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 variable
  binding and fresh name generation, especially the representation of, 
  and reasoning about, datatypes defined from binding signatures.

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

SUBMISSION

Submissions are encouraged in one of the following three categories:

+ Category A: Detailed and technical accounts of new research, up to
  twelve pages including bibliography and appendices.

+ Category B: Shorter accounts of work in progress and proposed
  further directions, including discussion papers, up to nine pages
  including appendices.

+ Category C: System descriptions presenting an implemented tool
  and its novel features: up to four 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 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.
The proceedings will be published by ACM's printing vendor,
Sheridan Printing, and they will appear in the ACM Digital Library.
We encourage authors to use the templates available on ACM's website:
http://www.acm.org/sigs/pubs/proceed/template.html.

Workshop papers will be selected by the following Program Committee:

James Cheney (University of Edinburgh, UK)
Roy L. Crole (University of Leicester, UK)
Joelle Despeyroux (INRIA, France)
Amy Felty (University of Ottawa, Canada)
Martin Hofmann (Ludwig-Maximilians-Universitaet Muenchen, Germany)
Marino Miculan (University of Udine, Italy)
Alberto Momigliano (University of Edinburgh, UK)
Randy Pollack (University of Edinburgh, UK)

REGISTRATION

For venue, registration and suggested accommodation see the ICFP 2005
web page at ****  http://www.cs.luc.edu/icfp/  ****

IMPORTANT DATES

Abstract submission:  23 May 2005 
Paper submission:     30 May 2005
Notification:          1 July 2005
Final Version:        12 July 2005
Workshop:             30 September 2005

For further details about the Workshop, including questions concerning
the relevance of submissions, please contact one of the organizers

+ Alberto Momigliano (U. Edinburgh, UK) 
  email: amomigl1@inf.ed.ac.uk
+ Ivan Scagnetto (U. Udine, Italy)
  email: scagnett@dimi.uniud.it
+ Alwen Tiu (INRIA, France)
  email: Alwen.Tiu@loria.fr