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:
“The American Constitution, one of the few modern political documents drawn up by men who were forced by the sternest circumstances to think out what they really had to face instead of chopping logic in a university classroom.”
—George Bernard Shaw (1856–1950)
“Nobody is so constituted as to be able to live everywhere and anywhere; and he who has great duties to perform, which lay claim to all his strength, has, in this respect, a very limited choice. The influence of climate upon the bodily functions ... extends so far, that a blunder in the choice of locality and climate is able not only to alienate a man from his actual duty, but also to withhold it from him altogether, so that he never even comes face to face with it.”
—Friedrich Nietzsche (1844–1900)