Publications on LCF and HOL

The acronym LCF originally abbreviated “Logic for Computable Functions", but it now designates an architecture for interactive theorem proving: logical inferences can only be made in a small section of code. Complicated heuristic proof procedures must convert the proofs they find into basic inferences that can be checked by this small trusted kernel. The point of this architecture is that it greatly reduces the possibility of soundness errors.

Cambridge LCF is the immediate predecessor of the HOL system. The main difference is that it implements not higher-order logic but domain theory. Built upon Robin Milner's Edinburgh LCF, it is an order of magnitude faster. Cambridge LCF introduced full predicate logic equipped with a comprehensive set of tactics and tacticals, including the still-popular chaining and resolution tactics. It introduced conversions for generic rewriting; see the first reference below. It also introduced theorem continuations, the subgoaling commands and many other features familiar to HOL users.

  1. L. C. Paulson.
    A Higher-Order Implementation of Rewriting. Sci. Computer Programming 3 (1983), 119–149. Publisher's version
  2. L. C. Paulson.
    Deriving Structural Induction in LCF. In: G. Kahn, D. B. MacQueen, G. Plotkin, editors, Semantics of Data Types (Springer, 1984), 197–214.
  3. L. C. Paulson.
    Verifying the Unification Algorithm in LCF. Sci. Computer Programming 5 (1985), 143–170.
  4. L. C. Paulson.
    Lessons Learned from LCF: a Survey of Natural Deduction Proofs. Computer J. 28 (1985), 474–479.
  5. L. C. Paulson.
    Logic and Computation: Interactive proof with Cambridge LCF. (Cambridge University Press, 1987).

Cambridge LCF is still available. It was the immediate predecessor of HOL88, whose sources are online here and here.

Last revised: 3 April, 2018

Lawrence C. PaulsonComputer LaboratoryUniversity of Cambridge