Nuprl as a Generic Theorem Prover
Roderick Moten · eCommons (Cornell University) · 1996
Logical Frameworks are one way to provide generic theorem provers. This paper describes another method using loose semantics. In the paper, we explain loose semantics, describes its use in building a programming calculus in the style of Back's refinement calculus, and relates the idea to Logical Framework or General Logic. Viewing Nuprl as a generic theorem prover using loose semantics can be used to describe the inference engine of Nuprl 4. This is the first attempt to explain the system design of Nuprl and relate it to the code.