AAn interactive '''theorem prover''' was developed at the universities of [[University of Edinburgh|Edinburgh]] and [[Stanford University|Stanford]] by [[Robin Milner]] and others.
ItLCF introduced the general purpose [[programming language]] [[ML programming language|ML]] to allow users to write theorem proving tactics.
Theorems in the system are propositionpropositions of a special "theorem" abstract type,.
theThe ML type system ensures that theorems are derived using only sound
inference rules.
Successors include: the
[[HOL theorem prover|HOL]], and [[Isabelle theorem prover|Isabelle]] theorem provers.
