Logic for Computable Functions: Difference between revisions

Revision as of 12:41, 25 July 2024

Latest revision as of 18:48, 19 March 2025

(One intermediate revision by one other user 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 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 ==