Books
- L. C. Paulson.
A Compiler Generator for Semantic Grammars. PhD. Thesis, Stanford University (1981). - L. C. Paulson.
Logic and Computation: Interactive proof with Cambridge LCF. (Cambridge University Press, 1987). - L. C. Paulson.
ML for the Working Programmer. (Cambridge University Press, 1991; second edition, 1996). - L. C. Paulson.
Isabelle: A Generic Theorem Prover. (Springer LNCS 828, 1994). - Tobias Nipkow, L. C. Paulson and Markus Wenzel.
Isabelle/HOL: A Proof Assistant for Higher-Order Logic (Springer LNCS 2283, 2002).
Last revised: 3 January, 2008