The Coq mailing list

[Marino Miculan <miculan AT dimi.uniud.it>]

Please post.
-marino
=======================================================
[*** Usual apologies for multiple copies ***]

                           Call for Papers
                     Second ACM SIGPLAN Workshop
     MEchanized Reasoning about Languages with variable bINding

                             MERLIN 2003

     Uppsala, Sweden, 26 August 2003 in association with PLI 2003

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

KEYWORDS

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
areas of:

  + The automation of the metatheory of programming languages,
    particularly work which involves variable binding and fresh name
    generation.

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


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 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 and the
Springer   Verlag  LNCS  guidelines.    Papers  should   be  submitted
electronically  as a  PostScript  or  PDF file  to  the email  address
merlin03 AT dimi.uniud.it.
  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)

REGISTRATION

For venue, registration and suggested accommodation see the PLI 2003
web page at ****  http://www.it.uu.se/pli03/  ****

IMPORTANT DATES

+ 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
****  
merlin03 AT dimi.uniud.it
  ****

======================================================================