Technical reports
Lessons learned from LCF
August 1984, 16 pages
DOI: 10.48456/tr-54
Abstract
The history and future prospects of LCF are discussed. The introduction sketches basic concepts such as the language ML, the logic PPLAMBDA, and backwards proof. The history discusses LCF proofs about denotational semantics, functional programs, and digital circuits, and describes the evolution of ideas about structural induction, tactics, logics of computation, and the use of ML. The biography contains thirty-five references.
Full text
PDF (1.3 MB)
BibTeX record
@TechReport{UCAM-CL-TR-54, author = {Paulson, Lawrence}, title = {{Lessons learned from LCF}}, year = 1984, month = aug, url = {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-54.pdf}, institution = {University of Cambridge, Computer Laboratory}, doi = {10.48456/tr-54}, number = {UCAM-CL-TR-54} }