Logic for Computable Functions (LCF) is an interactive automated theorem prover developed at the universities of Edinburgh and Stanford by Robin Milner and others in 1972. LCF introduced the general-purpose programming language ML to allow users to write theorem-proving tactics. Theorems in the system are propositions of a special "theorem" abstract datatype. The ML type system ensures that theorems are derived using only the inference rules given by the operations of the abstract type.