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

Special issue of JFP - Logical Frameworks and Meta-languages

The Journal of Functional Programming

                           CALL FOR PAPERS

          Special issue on LOGICAL FRAMEWORKS AND METALANGUAGES

           http://www-sop.inria.fr/certilab/LFM00/cfp-jfp.html

Logical frameworks and meta-languages are intended as a common
substrate for representing and implementing a wide variety of logics
and formal systems.  Their definition and implementation have been the
focus of considerable work over the last decade.  At the heart of this
work is a quest for generality: A logical framework provides a basis
for capturing uniformities across deductive systems and support for
implementing particular systems.  Similarly a meta-language supports
reasoning about and using languages.

  Logical frameworks have been based on a variety of different languages
including higher-order logics, type theories with dependent types,
linear logic, and modal logic. Techniques of representation of logics
include higher-order abstract syntax, inductive definitions or some
form of equational or rewriting logic in which substitution is
explicitly encoded.

  Examples of systems that implement logical frameworks include Alf,
Coq, NuPrl, HOL, Isabelle, Maude, lambda-Prolog, and Twelf.  An
active area of research in such systems is the study of automated
reasoning techniques.  Current work includes the development of
various automated procedures as well as the investigation of rewriting
tools that use reflection or make use of links with systems that
already have sophisticated rewriting systems.  Program extraction and
optimization are additional topics of ongoing work.

  The Workshop on Logical Frameworks and Meta-languages LFM'2000
(see http://www-sop.inria.fr/certilab/LFM00/) will be
held as part of the International Conference on Logic in Computer
Science (LICS'2000) at Santa Barbara in June 2000.
This workshop will bring together designers, implementers, and
practitioners to discuss the development of logical frameworks and
their use in meta-reasoning and programming.

  As a followup to this workshop, a special issue on this topic will be
published by the Journal of Functional Programming.  Papers presenting
original contributions on any aspect of logical frameworks and
meta-languages are solicited.  Topics of interest include (but are not
limited to):

    the design of logical frameworks,
    meta-theoretical studies,
    comparative studies,
    implementation,
    techniques of representation of formal systems,
    proofs of properties of formal systems,
    program development and proofs of program correctness.

  All contributors to LFM'2000 are invited to submit a full paper, but
the special issue is open to everyone.  Manuscripts should be
unpublished works and not submitted elsewhere.  Revised and enhanced
versions of papers published in conference proceedings that have not
appeared in archival journals are eligible for submission.  All
submissions will be reviewed according to the usual standards of
scholarship and originality.  Information on JFP submissions can be
found at URL http://www.dcs.gla.ac.uk/jfp/.
Please use the JFP Latex style files.
There is no fixed page limit; Typical JFP papers are about 25 to 30 
pages long.

  Submissions should be sent to both guest editors (addresses below),
with a copy to Nasreen Ahmad (nasreen@dcs.gla.ac.uk). Submitted
articles should be sent in postscript format preferably gzipped and
uuencoded. In addition, please send, as plain text, title, abstract,
and contact information. The submission deadline is October 23, 2000.

  Guest Editors:
  Joëlle Despeyroux, INRIA, Joelle.Despeyroux@inria.fr
  Robert Harper, CMU, Robert.Harper@cs.cmu.edu