The Coq mailing list

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

Please post,
- Furio

=================================================
[ Usual apologies for multiple copies ]

                           Special Issue of
                Higher-Order and Symbolic Computation
                                  on
      MEchanized Reasoning about Languages with variable bINding

       (Following the Second ACM SIGPLAN Workshop MERLIN 2003)
                     http://merlin.dimi.uniud.it

                   Editor in chief: Carolyn Talcott
             Guest Editor: Furio Honsell (Univ. of Udine)


KEYWORDS

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

SCOPE AND AIMS

Currently, there is considerable interest in the use of computerized
tools to encode and reason formally on 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, (co)inductive
definitions, and associated schemes of (co)recursion.

Following the successful workshop MERLIN 2003 (held in conjunction
with PLI'03), we seek contributions, to be collected in a Special
Issue of Higher-Order and Symbolic Computation, 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 and manipulating
  variable and name 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 and name 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.

Both research and tutorial/surveys papers are welcome.
Submissions are not restricted to papers presented at the workshop.
Authors are invited to send their contribution, as a PDF or a PS file,
to the address   
merlin03 AT dimi.uniud.it
   by

                    ***   March 31, 2004.   ***

Authors are also invited to email us title, authors and a short
abstract in plain text before February 29, 2004.


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