Logic for Computable Functions

See also: Logic of Computable Functions

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.

References

Gordon, Michael J. C. (1996). "From LCF to HOL: a short history". Retrieved 2007-10-11.
Milner, Robin (May 1972). Logic for Computable Functions: description of a machine implementation. (PDF). Stanford University.

This article is issued from Wikipedia - version of the Thursday, April 03, 2014. The text is available under the Creative Commons Attribution/Share Alike but additional terms may apply for the media files.