Skip to main content
PRL Project

The Nuprl 5 Library

by Richard Eaton

The Nuprl 5 library is a framework for storage and retrieval of logical data. The library will be suitable as a repository for proofs developed in any theorem proving system.

I will discuss the implementation from a traditional database viewpoint and as a method of implementing working maps a'la Stuart.