Implementing Mathematics with The Nuprl Proof Development System by R. L. Constable, at al.
Publisher: Prentice Hall 1986
ISBN/ASIN: 0134518322
ISBN-13: 9780134518329
The authors offer a tutorial on the new mathematical ideas which underlie their research. In doing so they have tried to provide several entry points into the material, even at the cost of considerable redundancy. Many of the ideas will be accessible to a well-trained undergraduate with a good background in mathematics and computer science.
Mathematics Applied Computer Mathematics