Jump to content

Logic for Computable Functions

From Wikipedia, the free encyclopedia
This is an old revision of this page, as edited by Cydebot (talk | contribs) at 14:25, 25 November 2007 (Robot - Moving category Theorem provers to Theorem proving software systems per CFD at Wikipedia:Categories for discussion/Log/2007 November 16.). The present address (URL) is a permanent link to this revision, which may differ significantly from the current revision.

LCF (Logic for Computable Functions) is an interactive automated theorem prover developed at the universities of Edinburgh and Stanford by Robin Milner and others. 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 and Isabelle.

References

  • Gordon, Michael J. C. (1996). "From LCF to HOL: a short history". Retrieved 2007-10-11.
Stub icon

This logic-related article is a stub. You can help Wikipedia by expanding it.

Retrieved from "https://en.wikipedia.org/w/index.php?title=Logic_for_Computable_Functions&oldid=173682513"