Theorem Provers are software tools to aid the process of proving theorems. A major activity as part of the Alvey SE Programme was the mounting of a number of theorem prover systems for the user community. The focus was primarily about proving theorems about programs (for example, that a particular program possesses a particular property).
Three systems, ML/LCF, IOTA and Boyer-Moore were acquired.
ML/LCF was mounted on a VAX and the Atlas 10 under UTS. Over 30 copies of the system were distributed. Much interest was aroused by Larry Paulson's (Cambridge) book on LCF. Larry Paulson produced a SUN version of the system which was also distributed by Informatics.
Chris Wadsworth attended the Edinburgh meeting in May 1985 to finalise the language Standard ML (SML). The standard was a consolidation of tried-and-trusted developments in the ML community since the original language was designed for the Edinburgh LCF project. Principal additions were: the data constructors and pattern matching facilities of HOPE, exception values, a richer and more systematic set of definition constructs, a module facility based on the latter, and I/O handling. The language has Alvey backing and was used for theorem proving work.
Philip Hedlund converted ML/LCF to Standard ML. A new parser and type checker were completed together with the basic system (code generator and run-time support). Then the 20 or so LCF sources files written in old ML were translated to Standard ML. The new SML/LCF was then distributed.
IOTA, built at Kyoto University, was a modular programming system which included a significant verification capability. As IOTA was written in an ancient dialect of LISP, a significant amount of work was done trying make it generally available. An attempt to port the original Standard Lisp implementation of IOTA encountered greater difficulties than were anticipated (differences between early and current versions of Standard Lisp) and was eventually abandoned when a simpler option became available. A version of IOTA ported to Kyoto Common Lisp (KCL) was obtained from Kyoto, together with distributions of KCL for the VAX and SUN workstations. Installation and testing was done by Manchester University with assistance from Chris Wadsworth.
Informatics also acted as the UK distribution agent for the Boyer-Moore theorem prover from the University of Texas.
