Logic for Computable Functions

A theorem prover developed at University of Edinborough 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.