The Coq mailing list

["MERLIN'03" <merlin03 AT dimi.uniud.it>]

[*** Usual apologies for multiple copies ***]

                           Last 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/  *
                  **********************************

IMPORTANT DATES

+ Deadline for paper submission                 Monday  16 June
+ Notification of acceptance by email   Monday  14 July
+ Deadline for submission of Camera Ready Copy  Thursday 31 July
+ Early registration                                    To be announced.
+ Workshop date                                         Tuesday 26 August

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.     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.
Accepted papers will be published in the ACM Digital Library; a
special issue of a major journal is under consideration.

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/  ****

For further details about the Workshop, including questions concerning
the relevance of submissions, please contact the organizers at
****  
merlin03 AT dimi.uniud.it
  ****

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


--
   Marino Miculan    - Dipartimento di Matematica e Informatica
Universita` di Udine - via delle Scienze 206 - 33100 Udine - Italy
vox: +39-043255-8486 - fax: +39-043255-8499  - mob: +39-3292606452
mailto:miculan AT dimi.uniud.it
    http://www.dimi.uniud.it/~miculan/