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:
“What avail all your scholarly accomplishments and learning, compared with wisdom and manhood? To omit his other behavior, see what a work this comparatively unread and unlettered man wrote within six weeks. Where is our professor of belles-lettres, or of logic and rhetoric, who can write so well?”
—Henry David Thoreau (1817–1862)
“The mind is a finer body, and resumes its functions of feeding, digesting, absorbing, excluding, and generating, in a new and ethereal element. Here, in the brain, is all the process of alimentation repeated, in the acquiring, comparing, digesting, and assimilating of experience. Here again is the mystery of generation repeated.”
—Ralph Waldo Emerson (1803–1882)