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, 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  merlin03@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, Chair)
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@dimi.uniud.it  ****

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