PRL Seminars

In this seminar, I present the design of the refiner for the Nuprl Proof Development System. The refiner is the component of Nuprl which carries out directives for constructing proofs. The design of the refiner is a listing of its components, specifications of their interfaces, and a description of the relationship between the components.

I plan to spend the majority of the seminar describing the specifications of the components which is the mathematical foundation of proof construction in Nuprl. Note that proof construction in Nuprl is independent of the Nuprl type theory.