Department of Computer Science and Technology

Technical reports

Lessons learned from LCF

Lawrence Paulson

August 1984, 16 pages


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

  author =	 {Paulson, Lawrence},
  title = 	 {{Lessons learned from LCF}},
  year = 	 1984,
  month = 	 aug,
  url = 	 {},
  institution =  {University of Cambridge, Computer Laboratory},
  number = 	 {UCAM-CL-TR-54}