Logic for Computable Functions: Difference between revisions

Revision as of 22:00, 17 March 2025

Latest revision as of 18:48, 19 March 2025

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