Logic of Computable Functions (LCF) is a

deductive system A formal system is an abstract structure and formalization of an axiomatic system used for deducing, using rules of inference, theorems from axioms. In 1921, David Hilbert proposed to use formal systems as the foundation of knowledge in math ...

for

computable function Computable functions are the basic objects of study in computability theory. Informally, a function is ''computable'' if there is an algorithm that computes the value of the function for every value of its argument. Because of the lack of a precis ...

s proposed by

Dana Scott Dana Stewart Scott (born October 11, 1932) is an American logician who is the emeritus Hillman University Professor of Computer Science, Philosophy, and Mathematical Logic at Carnegie Mellon University; he is now retired and lives in Berkeley, C ...

in 1969 in a memorandum unpublished until 1993. It inspired: *

Logic for Computable Functions Logic for Computable Functions (LCF) is an interactive automated theorem prover developed at Stanford and Edinburgh by Robin Milner and collaborators in early 1970s, based on the theoretical foundation of logic of computable functions previously ...

(LCF), theorem proving logic by

Robin Milner Arthur John Robin Gorell Milner (13 January 1934 – 20 March 2010) was a British computer scientist, and a Turing Award winner.Programming Computable Functions In computer science, Programming Computable Functions (PCF), or Programming with Computable Functions, or Programming language for Computable Functions, is a programming language which is typed and based on functional programming, introduced by G ...

(PCF), small theoretical programming language by

Gordon Plotkin Gordon David Plotkin (born 9 September 1946) is a theoretical computer scientist in the School of Informatics at the University of Edinburgh. Plotkin is probably best known for his introduction of structural operational semantics (SOS) and his ...

.{{ cite journal , first = Gordon D. , last = Plotkin , authorlink = Gordon Plotkin , title = LCF considered as a programming language , journal = Theoretical Computer Science , year = 1977 , pages = 223–255 , volume = 5 , issue = 3 , doi = 10.1016/0304-3975(77)90044-5 , url = http://homepages.inf.ed.ac.uk/gdp/publications/LCF.pdf , doi-access = free

References

Programming language theory