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 and includes full predicate logic, a full set of tactics and tacticals, a generic rewriter based upon the notion of conversion, theorem continuations, 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.
  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.

Last revised: 29 October, 2013
Lawrence C. PaulsonComputer LaboratoryUniversity of Cambridge