Professor Constable has released a paperback version of Implementing Mathematics with the Nuprl Proof Development System. The book, written in 1985 by the PRL Team, serves as a manual to using the Nuprl system as well as an introduction to formal logic in computer science and its use in program development and verification.
The book is available from Amazon and other retailers.
