Logic for Computable Functions: Difference between revisions

Revision as of 19:18, 29 February 2024

Latest revision as of 18:48, 19 March 2025

(4 intermediate revisions by 4 users not shown)

Line 1:

{{Short description|1970s automated theorem prover}}

{{see also|Logic of Computable Functions}}

'''Logic for Computable Functions''' ('''LCF''') is an interactive [[automated theorem prover]] developed at [[Stanford University|Stanford]] and [[University of Edinburgh|Edinburgh]] by [[Robin Milner]] and collaborators in early 1970s, based on the theoretical foundation of [[Logic of Computable Functions|logic '''of''' computable functions]] previously proposed by [[Dana Scott]]. Work on the LCF system introduced the general-purpose [[programming language]] [[ML (programming language)|ML]] to allow users to write theorem-proving tactics, supporting [[algebraic data type]]s, [[parametric polymorphism]], [[abstract data types]], and [[Exception handling|exceptions]].

== Basic idea ==

Line 15:

=== Trusted computing base ===

The implementation of the underlying ML compiler adds to the [[trusted computing base]]. Work on CakeML<ref name="cakeml">{{cite web |title=CakeML |url=https://cakeml.org/ |access-date=2 November 2019}}</ref> resulted in a formally verified ML compiler, alleviating some of these concerns.

=== Efficiency and complexity of proof procedures ===

Line 23:

== Influences ==

Among subsequent implementations is Cambridge LCF. Later systems simplified the logic to use total instead of partial functions, leading to [[HOL (proof assistant)|HOL]], [[HOL Light]], and the [[Isabelle proof assistant]] that supports various logics. As of 2019, the Isabelle [[proof assistant]] still contains an implementation of an LCF logic, Isabelle/LCF.

== Notes ==

Line 74:

|publisher=Stanford University

|date=May 1972

|url=httphttps://wwwapps.dtic.mil/dtic/tr/fulltextsti/u2pdfs/785072AD0785072.pdf}}

* {{cite book

|last=Milner

Line 91:

{{ML programming}}

{{Mathlogic-stub}}

[[Category:Logic in computer science]]

[[Category:Proof assistants]]

{{Mathlogic-stub}}