PRL Math Library
Recent Library Updates

Work in Progress
a snapshot of Nuprl library objects. ongoing 
Constructive Reading of Classical Logic
by Robert L. Constable and Sarah Sernaker
July 2015

Logical Investigations, with the Nuprl Proof Assistant
by Robert L. Constable and Anne Trostle
July 2014

A Fast Algorithm for the Integer Square Root
by Anne Trostle and Mark Bickford
June 2014

Finding the Maximum Segment Sum
by Anne Trostle January 2014

An Algorithm for the Greatest Common Divisor
by Anne Trostle October 2013

Intuitionisitc Mathematics and Logic
by Joan Rand Moschovakis and Garyfallia Vafeiadou

Formalizing Constructive Analysis in Nuprl
by Mark Bickford Sept 20, 2012
This is a library of fully formalized definitions and proofs. Some of the material has been enhanced by the addition of informal explanations referring to it.
Browse by shelf view  orig sort  title  date  author  subject
55 results