The Structure of Nuprl's Type Theory
by Robert L. Constable
Logic of Computation, M. Broy and H. Schwichtenberg (eds.), pp. 123-156, Springer-Verlag
After my lectures on this topic were delivered in July 1995 at Marktoberdorf, my colleagues and I made available much more related material both at the Nuprl home page on the World Wide Web www.nuprl.org and in publications, some soon to appear.
At the Web site the thesis of Jackson and the article by Forester are especially relevant to my lecture. Also, the 1986 Nuprl book is now available on line at the Web site as is the Nuprl 4 reference manual and a host of Nuprl libraries.
As a result of the ready access to this material and because the material in the Cornell Technical Report series is part of an expanding digital library whose longevity seems guaranteed, I designed this article to concentrate on the material not available elsewhere, e.g., a discussion of the Core Theory and its relation to Nuprl 4.
A naive account of Core Type Theory is especially simple, and I think it provides a bridge to understanding the more daunting axiomatization of the Nuprl type theory which is used in all of the on-line libraries. This article presents the Core Theory and relates it to a corresponding part of Nuprl. Comparisons are made to set theory as a way to motivate the concepts.
bibTex ref: Con97