Nuprl Projects funded by

The Office of Naval Research (ONR) has funded basic work on the Nuprl constructive type theory since 1987. Many of the basic discoveries and advances made with this funding are now part of the Nuprl 4 and Nuprl 5 versions of the Proof Development System. This system is used in many ways at Cornell University and elsewhere.

ONR encouraged our efforts to provide access to Nuprl via the World Wide Web and has specifically enabled the creation of the Web based libraries and the Web browser used to present the Nuprl 4.2 libraries.

Currently ONR supported our work on computational complexity in type theory and the related topic of defining partial objects by axiomatizing an abstract notion of computation in type theory. The results are already being applied to programming language semantics in Karl Crary's work on the language KML, a dialect of ML with objects. Recent theoretical results can be read in the paper by Constable, Computational Complexity in Constructive Type Theory, in the list of publications and in the papers of Karl Crary available at his home page.

Two aspects of the ONR support are visible in the library of formal theorems about partial computable functions in a library called "bar types" under the Nuprl 4.2 libraries section. This library formalizes the results from the article by Constable and Smith in the journal Theoretical Computer Science, and it uses the Web browser developed with ONR support.

Currently ONR is the agent for our University Research Initiative (URI) project, Building Interactive Digital Libraries of Formal Algorithmic Knowledge.

---