Publications on LCF and HOL

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 the immediate predecessor of the HOL system. The main difference is that it implements not higher-order logic but domain theory. Built upon 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.

Cambridge LCF is still available.