CfP: ACM SIGPLAN MERLIN 2003
Call for Papers
Second ACM SIGPLAN Workshop
MEchanized Reasoning about Languages with variable bINding
Uppsala, Sweden, 26 August 2003 in association with PLI 2003
* http://merlin.dimi.uniud.it/ *
Induction and Coinduction, Logical Frameworks, Mechanization,
Metaprogramming, Operational Semantics, Programming Languages, Theorem
Proving, Variable Binding.
SCOPE AND AIMS
Currently, there is considerable interest in the use of computers to
encode (operational) semantic descriptions of programming languages.
Such encodings are often done within the metalanguage of a theorem
prover or related system. The encodings may require the use of
variable binding constructs, inductive definitions, coinductive
definitions, and associated schemes of (co)recursion. The broad aims
are to run a short, but highly focused 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 the
+ The automation of the metatheory of programming languages,
particularly work which involves variable binding and fresh name
+ Theoretical and practical problems of encoding variable binding,
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.
Submissions are encouraged in one of the following three categories:
+ Category A: Detailed and technical accounts of new research, up to
fifteen pages including appendices.
+ Category B: Shorter accounts of work in progress and proposed
further directions, including discussion papers, up to ten pages
+ 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 and the
Springer Verlag LNCS guidelines. Papers should be submitted
electronically as a PostScript or PDF file to the email address
email@example.com. 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.
Workshop papers will be selected by the following Program Committee:
Simon Ambler (University of Leicester)
Furio Honsell (University of Udine)
Marino Miculan (University of Udine, Italy)
Dale Miller (INRIA/Futurs, France)
Ugo Montanari (University of Pisa, Italy)
Tobias Nipkow (Technische Universität München Germany)
Andrew M. Pitts (University of Cambridge, UK)
Carsten Schürmann (Yale University, USA)
For venue, registration and suggested accommodation see the PLI 2003
web page at **** http://www.it.uu.se/pli03/ ****
+ Monday June 16th Deadline for paper submission.
+ Monday July 14th Notification of acceptance by email.
+ Thursday July 31st Deadline for submission of Camera Ready Copy.
+ Early registration To be announced.
+ Workshop dates August 26th 2003.
For further details about the Workshop, including questions concerning
the relevance of submissions, please contact the organizers at
**** firstname.lastname@example.org ****