The Journal of Functional Programming

Editorial January 2000

CALL FOR PAPERS

Special issue on Logical Frameworks and Metalanguages

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) 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):

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 here. 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. For other submission details, please consult an issue of the Journal of Functional Programming or see the Journal's web pages.

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