PRL Seminars

The refiner is the inference mechanism of the Nuprl proof development system. For several months I have been rewriting the refiner in SML from Lisp. Much of this effort has been spent writing an informal, but rigorous, specification for the refiner. In today's seminar, I will be giving a high level description of the design of the SML implementation of the refiner based on the specification. New and potential users of Nuprl may find this discussion as a helpful overview of Nuprl.