Logic of Computable Functions (LCF) is a

deductive system A formal system is an abstract structure used for inferring theorems from axioms according to a set of rules. These rules, which are used for carrying out the inference of theorems from axioms, are the logical calculus of the formal system. A form ...

for

computable function Computable functions are the basic objects of study in computability theory. Computable functions are the formalized analogue of the intuitive notion of algorithms, in the sense that a function is computable if there exists an algorithm that can do ...

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, Ca ...

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), known as Robin Milner or A. J. R. G. Milner, was a British computer scientist, and a Turing Award winner.

. *

Programming Computable Functions In computer science, Programming Computable Functions (PCF) is a typed functional language introduced by Gordon Plotkin in 1977, based on previous unpublished material by Dana Scott. It can be considered to be an extended version of the typed lamb ...

(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 hi ...

.{{ 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