Implementing Mathematics with the Nuprl Development System

http://www.cs.cornell.edu/Info/Projects/NuPrl/book/doc.html

by Robert L. Constable, Stuart F. Allen, H. M. Bromley, Walter Rance Cleaveland, J. F. Cremer, Robert W. Harper, Douglas J. Howe, Todd B. Knoblock, Nax P. Mendler, Prakash Panangaden, James T. Sasaki, and Scott F. Smith

Prentice-Hall:NJ, 1986.