Innovations in Computational Type Theory using Nuprl

Stuart Allen, Mark Bickford, Robert Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo, Evan Moran.

Journal of Applied Logic4(4):428-469, 2006


Abstract

For twenty years the Nuprl (``new pearl'') system has been used to develop software systems and formal theories of computational mathematics. It has also been used to explore and implement computational type theory (CTT) -- a formal theory of computation closely related to Martin-Láf's intuitionistic type theory (ITT) and to the calculus of inductive constructions (CIC) implemented in the Coq prover.

This article focuses on the theory and practice underpinning our use of Nuprl for much of the last decade. We discuss innovative elements of type theory, including new type constructors such as unions and dependent intersections, our theory of classes, and our theory of event structures.

We also discuss the innovative architecture of Nuprl as a distributed system and as a transactional database of formal mathematics using the notion of abstract object identifiers. The database has led to an independent project called the Formal Digital Library, FDL, now used as a repository for Nuprl results as well as selected results from HOL, MetaPRL, and PVS. We discuss Howe's set theoretic semantics that is used to relate such disparate theories and systems as those represented by these provers.


PS Version PDF Version   (Preprint) BACK
Back to overview of papers


Bibtex Entry

@Article{ar:Allen+06a, author = "Stuart Allen and Mark Bickford and Robert Constable and Richard Eaton and Christoph Kreitz and Lori Lorigo and Evan Moran", title = "Innovations in Computational Type Theory using {Nuprl}", journal = "Journal of Applied Logic", year = "2006", volume = "4", number = "4", pages = "428--469", }