[Prev][Next][Index][Thread]
Special Issue of JFP on Theorem Proving
CALL FOR PAPERS
Journal of Functional Programming
Special Issue on Theorem Provers and Functional Programming
A special issue of the Journal of Functional Programming will be
devoted to the use of functional programming in theorem proving. The
submission deadline is 31 August 1997.
The histories of theorem provers and functional languages have been deeply
intertwined since the advent of Lisp. A notable example is the ML family
of languages, which are named for the meta language devised for the LCF
theorem prover, and which provide both the implementation platform and
interaction facilities for numerous later systems (such as Coq, HOL,
Isabelle, NuPrl). Other examples include Lisp (as used for ACL2, PVS,
Nqthm) and Haskell (as used for Veritas).
This special issue is devoted to the theory and practice of using
functional languages to implement theorem provers and using theorem provers
to reason about functional languages. Topics of interest include, but are
not limited to:
* architecture of theorem prover implementations
* interface design in the functional context
* limits of the LCF methodology
* impact of host language features
- type systems
- lazy vs strict languages
- imperative (impure) features
* performance problems and solutions
* problems of scale
* special implementation techniques
- term representations (e.g. de Bruijn vs name carrying vs BDDs)
* limitations of current functional languages
* mechanised theories of functional programming
Particularly welcome are papers of interest to both the functional
programming and theorem proving communities and which deal with systems in
which the influence of the functional context is substantive and
interesting. Papers should aim to go beyond mere system descriptions.
Submission of PostScript by email is encouraged, but hard copies are also
welcome. All submissions for the special issue on implementing theorem
provers should be sent to the Guest Editor (see address below).
Submissions should arrive by 31 August 1997. For other submission details,
please consult an issue of the Journal of Functional Programming or see the
Journal's web pages at http://www.dcs.gla.ac.uk/jfp/.
GUEST EDITOR
Dr. Tom Melham
Department of Computing Science
University of Glasgow
Glasgow, Scotland, G12 8QQ
Tel: +44 141 330 4967 [direct line]
Fax: +44 141 330 4913
Email: tfm@dcs.gla.ac.uk
WWW: http://www.dcs.glasgow.ac.uk/~tfm/
+--------------------------------------------------------------------------+