Skip to main content
PRL Project

The Book

Implementing Mathematics with The Nuprl Proof Development System

Important note about this book

The Nuprl math library is constantly evolving, expanding, and refining. This text, written in 1985, provides useful descriptions and background information for using Nuprl. However many of the mathemacial projections have been updated and no longer exist in the library . Please see the Math Library and Publications list for more recent projections.


Implementing Mathematics with The Nuprl Proof Development System

By the PRL Group:
R. L. Constable
S. F. Allen
H. M. Bromley
W. R. Cleaveland
J. F Cremer
R. W. Harper
D. J. Howe
T. B. Knoblock
N. P. Mendler
P. Panangaden
J. T Sasaki
S. F. Smith

Implementing Mathematics with The Nuprl Proof Development System
Available from Amazon and other retailers.

This research supported in part by the National Science Foundation under grant DCR83-03327.
Copyright © 1985 by R. L. Constable and Prentice-Hall.