Logic for Computable Functions: Difference between revisions

Revision as of 02:54, 23 January 2023

Latest revision as of 18:48, 19 March 2025

(5 intermediate revisions by 5 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 31:

{{Refbegin}}

* {{cite book

| last1 = Gordon

| first1 = Michael J.

| author1-link = Michael J. C. Gordon

| last2 = Milner

| first2 = Arthur J.

| last3 = Wadsworth

| first3 = Christopher P.

| date = 1979

| title = Edinburgh LCF: A Mechanised Logic of Computation

| doi = 10.1007/3-540-09724-4

| series = Lecture Notes in Computer Science

| volume = 78

| publisher = Springer |___location=Berlin Heidelberg

| isbn = 978-3-540-09724-2 | s2cid = 21159098

}}

* {{cite book

| last = Gordon

| first = Michael J. C.

| chapter = From LCF to HOL: a short history

| url = http://www.cl.cam.ac.uk/~mjcg/papers/HolHistory.html

| access-date = 2007-10-11 |title=Proof, language, and interaction

|pages=169–185

|publisher=MIT Press
|___location=Cambridge, MAMassachusetts
|date=2000

|isbn=0-262-16188-5 }}

|access-date=2007-10-11}}

* {{cite book

| last1 = Loeckx

| first1 = Jacques

| last2 = Sieber

| first2 = Kurt

| date = 1987

| title = The Foundations of Program Verification

| doi = 10.1007/978-3-322-96753-4

| edition = 2nd

| publisher = Vieweg+Teubner Verlag

| isbn = 978-3-322-96754-1 }}

* {{cite manual

|last=Milner |first=Robin |author -link=Robin Milner, Robin

| title = Logic for Computable Functions: description of a machine implementation.

| publisher = Stanford University

| date = May 1972

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

* {{cite book

| last = Milner

| first =Robin |author-link=Robin Milner

| editor = Bečvář, Jiří

| date = 1979

| title = Mathematical Foundations of Computer Science 1979

| chapter = Lcf: A way of doing proofs with a machine

| pages = 146–159

| doi = 10.1007/3-540-09526-8_11

| series = Lecture Notes in Computer Science

| volume = 74

| publisher = Springer |___location=Berlin Heidelberg

| isbn = 978-3-540-09526-2}}

{{Refend}}

{{Mathlogic-stubML programming}}

[[Category:Logic in computer science]]

[[Category:Proof assistants]]

{{Mathlogic-stub}}