Call for papers: HOSC Special Issue following MERLIN 2003

Please post,
- Marino

[ Usual apologies for multiple copies ]

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

        (Following the Second ACM SIGPLAN Workshop MERLIN 2003)

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


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


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

+ 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

		    ***   March 31, 2004.   ***

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