Logic of Computable Functions

The printable version is no longer supported and may have rendering errors. Please update your browser bookmarks and please use the default browser print function instead.

This computer science article is a stub. You can help Wikipedia by expanding it.

Logic of Computable Functions (LCF) is a deductive system for computable functions proposed by Dana Scott in 1969 in a memorandum unpublished until 1993.^[1] It inspired:

Logic for Computable Functions (LCF), theorem proving logic by Robin Milner.^[2]
Programming Computable Functions (PCF), small theoretical programming language by Gordon Plotkin.^[3]

References

^ Dana S. Scott. "A type-theoretical alternative to ISWIM, CUCH, OWHY". Theoretical Computer Science, 121:411–440, 1993. Annotated version of the 1969 manuscript.
^ Robin Milner (1973). "Models of LCF"
^ Plotkin, Gordon D. (1977). "LCF considered as a programming language" (PDF). Theoretical Computer Science. 5 (3): 223–255. doi:10.1016/0304-3975(77)90044-5.

[1] Dana S. Scott. "A type-theoretical alternative to ISWIM, CUCH, OWHY". Theoretical Computer Science, 121:411–440, 1993. Annotated version of the 1969 manuscript.

[2] Robin Milner (1973). "Models of LCF"

[3] Plotkin, Gordon D. (1977). "LCF considered as a programming language" (PDF). Theoretical Computer Science. 5 (3): 223–255. doi:10.1016/0304-3975(77)90044-5.

[1]

[2]

[3]