Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
Publications of L C Paulson: LCF & HOL
[go: Go Back, main page]

Publications on LCF and HOL

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.
  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: 26 February, 2010