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 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.

References

{{subst:#ifeq:{{{header}}}|1|==Speedy deletion nomination of [[:{{{1}}}]]==}}

You may wish to consider using a Wizard to help you create articles. See the Article Wizard.

Thank you.

The article [[:{{{1}}}]] has been speedily deleted from Wikipedia. This was done because the article was about a real person or group of people, individual animal, organization (band, club, company, etc.), web content or an organized event, but did not indicate how or why the subject is important or significant: that is, why an article about that subject should be included in an encyclopedia. Under the section A7 of the criteria for speedy deletion, such articles may be deleted at any time. If you can indicate why the subject is actually significant enough for an encyclopedia article, you are free to re-create it, but this time you need to demonstrate that, which is best done by citing to reliable, secondary sources that are entirely unconnected to the topic.

Please see the guidelines for what is generally accepted as notable, and for specific types of articles, you may want to check out our criteria for biographies, for web sites, for musicians, or for companies. Feel free to leave a note on my talk page if you have any questions about this. Template:J

• Template:Cnimñnonbnmte book
• Gordon, Michael J. C. (1996). "From LCF to HOL: a short history". 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ří (ed.). Mathematical Foundations of Computer Science 1979. Lecture Notes in Computer Science. Vol. 74. Springer Berlin Heidelberg. pp. 146–159. doi:10.1007/3-540-09526-8_11. ISBN 978-3-540-09526-2. Retrieved 16 February 2016.