Nuprl is a system supporting the interactive development of formal mathematics. It was designed to be especially suited to computationally significant mathematics and to the construction of formally verified software. The implementation of Nuprl, funded by the NSF, was completed in 1984. Since then the system has been used extensively at Cornell and elsewhere as a basis for further research. This research has resulted in significant advances in the areas of automated reasoning and computational logic. The system has been successfully applied to a wide range of problems, from verification of computer hardware to an open problem in the theory of programming languages. It has been the subject of many articles and PhD theses. The goal of the present project is to rewrite parts of the system in order to incorporate certain extensions (a reflection mechanism) and improvements (new definition facility). These are based on several years of study and experience with the system. They will make the system more accessible, both to researchers in the area and to others such as mathematicians and educators. With the implementation of the reflection mechanism, Nuprl will be applicable to domains that are currently difficult to treat.
