[Prev][Next][Index][Thread]
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
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@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.
=================================================