[Prev][Next][Index][Thread]

MERLIN 2001 Call for Papers



[ The following workshop may be of interest to TYPES readers because
types play a key role within programming languages (involving variable
binding), and because type theory underpins many of the tools used for
reasoning about programming languages. ] 


                           Call for Papers
                          
                             Workshop on
		
     MEchanized Reasoning about Languages with variable bINding
				     
                            (MERLIN 2001)  
				     
    Siena, Italy, June 18-19, 2001 in connection with IJCAR 2001

                  **********************************
                  * http://www.mcs.le.ac.uk/merlin *
                  **********************************

KEYWORDS 

Induction and Coinduction, Logical Frameworks, Mechanization,
Metaprogramming, Operational Semantics, Programming Languages, Theorem
Proving, Variable Binding.

JUSTIFICATION

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

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

INVITED TALK

Andrew Pitts, University of Cambridge, has agreed to give an invited
talk on "A First Order Theory of Names and Binding".

SUBMISSION

Submissions are encouraged in one of the following two 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.

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 or B) must be clearly indicated.  Authors are
encouraged to use LaTeX and the Springer Verlag LNCS
guidelines. Papers should be submitted electronically as a PostScript
file to the address merlin@mcs.le.ac.uk. If necessary, authors may
submit three hard copies to the Local Organizer, Alberto Momigliano,
by surface mail.

Workshop papers will be selected by the following Program Committee:

  Simon Ambler (University of Leicester)
  Roy Crole (Chair; University of Leicester) 
  Amy Felty (University of Ottawa)
  Andrew Gordon (Microsoft Research, Cambridge)
  Furio Honsell (University of Udine)
  Tom Melham (University of Glasgow)
  Frank Pfenning (Carnegie Mellon University)
 
REGISTRATION

For venue, registration and suggested accommodation see the IJCAR 2001
web page at **** http://www.dii.unisi.it/~ijcar/ ****

IMPORTANT DATES

+ Friday March 30th	Deadline for paper submission.
+ Friday April 20th	Notification of acceptance by email. 
+ Friday May 18th	Deadline for submission of Camera Ready Copy. 
+ Early registration	To be announced.
+ Workshop dates	June 18-19 2001, exact date to be confirmed.

For further details about the Workshop, including questions concerning
the relevance of submissions, please contact one of

+  Roy L. Crole, email: R.Crole@mcs.le.ac.uk
+  Simon J. Ambler, email: S.Ambler@mcs.le.ac.uk
+  Alberto Momigliano (Local Organizer), email: A.Momigliano@mcs.le.ac.uk
 
at postal address:

Department of Mathematics and Computer Science,  
University of Leicester,  
University Road,  
LEICESTER,  
LE1 7RH,   
United Kingdom.