[TYPES] CFP: MERLIN'05 at ICFP'05
Alwen Tiu
Alwen.Tiu at loria.fr
Wed Apr 6 11:40:55 EDT 2005
[Apologies for cross-postings. Please send to interested colleagues and students]
-------------- next part --------------
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
fifteen pages including bibliography but excluding appendices.
+ Category B: Shorter accounts of work in progress and proposed
further directions, including discussion papers, up to ten pages
including 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 merlin at 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 at inf.ed.ac.uk
+ Ivan Scagnetto (U. Udine, Italy)
email: scagnett at dimi.uniud.it
+ Alwen Tiu (INRIA, France)
email: Alwen.Tiu at loria.fr
More information about the Types-list
mailing list