The LCF theorem prover reference article from the English Wikipedia on 24-Apr-2004 (provided by Fixed Reference: snapshots of Wikipedia from wikipedia.org)

LCF theorem prover

An interactive theorem prover developed at the universities of Edinburgh and Stanford by Robin Milner and others. LCF introduced the general purpose programming language ML to allow users to write theorem proving tactics. Theorems in the system are propositions of a special "theorem" abstract type. The ML type system ensures that theorems are derived using only sound inference rules.

Successors include the HOL and Isabelle theorem provers.

This is the "LCF theorem prover" reference article from the English Wikipedia. All text is available under the terms of the GNU Free Documentation License. See also our Disclaimer.