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.
Successors include HOL (Higher Order Logic) and Isabelle.
Famous quotes containing the words logic and/or functions:
“You can no more bridle passions with logic than you can justify them in the law courts. Passions are facts and not dogmas.”
—Alexander Herzen (1812–1870)
“Those things which now most engage the attention of men, as politics and the daily routine, are, it is true, vital functions of human society, but should be unconsciously performed, like the corresponding functions of the physical body.”
—Henry David Thoreau (1817–1862)