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