A
theorem prover was developed at
University of Edinburgh by
Robin Milner.
It introduced the general purpose
programming language ML to allow users to write theorem proving tactics.
Theorems are proposition of special "theorem" type,
the ML type system ensures that theorems are derived using only sound
inference rules.
Successors include:
HOL theorem prover, Isabelle theorem prover.