Logic for Computable Functions

From Wikipedia, the free encyclopedia
  (Redirected from LCF theorem prover)
Jump to navigation Jump to search

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 terms of a special "theorem" abstract data type. 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.


  • Gordon, Michael J.; Milner, Arthur J.; Wadsworth, Christopher P. (1979). Edinburgh LCF: A Mechanised Logic of Computation. Lecture Notes in Computer Science. 78. Berlin Heidelberg: Springer. doi:10.1007/3-540-09724-4. ISBN 978-3-540-09724-2.
  • Gordon, Michael J. C. (2000). "From LCF to HOL: a short history". Proof, language, and interaction. Cambridge, MA: MIT Press. pp. 169–185. ISBN 0-262-16188-5. Retrieved 2007-10-11.
  • Loeckx, Jacques; Sieber, Kurt (1987). The Foundations of Program Verification (2nd ed.). Vieweg+Teubner Verlag. doi:10.1007/978-3-322-96753-4. ISBN 978-3-322-96754-1.
  • Milner, Robin (May 1972). Logic for Computable Functions: description of a machine implementation (PDF). Stanford University.
  • Milner, Robin (1979). "Lcf: A way of doing proofs with a machine". In Bečvář, Jiří. Mathematical Foundations of Computer Science 1979. Lecture Notes in Computer Science. 74. Berlin Heidelberg: Springer. pp. 146–159. doi:10.1007/3-540-09526-8_11. ISBN 978-3-540-09526-2.
Retrieved from "https://en.wikipedia.org/w/index.php?title=Logic_for_Computable_Functions&oldid=813348289"
This content was retrieved from Wikipedia : http://en.wikipedia.org/wiki/LCF_theorem_prover
This page is based on the copyrighted Wikipedia article "Logic for Computable Functions"; it is used under the Creative Commons Attribution-ShareAlike 3.0 Unported License (CC-BY-SA). You may redistribute it, verbatim or modified, providing that you comply with the terms of the CC-BY-SA