- Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, Engelwood Cliffs, NJ, 1986 (with PRL Group).
- An Introduction to the PL/CV2 Programming Logic. In Lecture Notes in Computer Science 135, Springer-Verlag, 1982 (with S. D. Johnson and C. D. Eichenlaub).
- A Programming Logic, Winthrop, Cambridge, 1978 (with M. J. O’Donnell).