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

        Co-Editors: Furio Honsell (University of Udine, Italy),
                    Carolyn Talcott (SRI International, USA)

             *** NOTICE: NEW DEADLINE: April 25, 2004 ***

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@dimi.uniud.it   by

                    ***   Sunday, April 25, 2004.   ***

Authors are also invited to email title, authors and a short
abstract in plain text before April 10, 2004.


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