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.
