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.