A theorem prover developed at University of Edinburgh by Robin Milner. It introduced a 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.