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.