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)
“Adolescents, for all their self-involvement, are emerging from the self-centeredness of childhood. Their perception of other people has more depth. They are better equipped at appreciating others’ reasons for action, or the basis of others’ emotions. But this maturity functions in a piecemeal fashion. They show more understanding of their friends, but not of their teachers.”
—Terri Apter (20th century)