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
Introduction to the Special Issue: Soft Power of Civil Society in International Relations