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: [EMAIL PROTECTED] WWW: http://www.dcs.glasgow.ac.uk/~tfm/ +--------------------------------------------------------------------------+