Nuprl
Nuprl is a proof development system, providing computer-mediated analysis and proofs of formal mathematical statements, and tools for software verification and optimization. Originally developed in the 1980s by Robert Lee Constable and others, the system is now maintained by the PRL Project at Cornell University. The currently supported version, Nuprl 5, is also known as FDL (Formal Digital Library). Nuprl functions as an automated theorem proving system and can also be used to provide proof assistance.
Design
[edit | edit source]Nuprl uses a type system based on Martin-Löf intuitionistic type theory to model mathematical statements in a digital library. Mathematical theories can be constructed and analyzed with a variety of editors, including a graphical user interface, a web-based editor, and an Emacs mode. A variety of evaluators and inference engines can operate on the statements in the library. Translators also allow statements to be manipulated with Java and OCaml programs.[1] The overall system is controlled with a variant of ML.
Nuprl 5's architecture is described as a "distributed open architecture",[1] and Nuprl 5 is intended primarily to be used as a web service rather than as standalone software.[citation needed]
History
[edit | edit source]Nuprl was first released in 1984, and was first described in detail in the book Implementing Mathematics with the Nuprl Proof Development System,[2] published in 1986. Nuprl 2 was the first Unix version. Nuprl 3 provided machine proof for mathematical problems related to Girard's paradox and Higman's lemma. Nuprl 4, the first version developed for the World Wide Web, was used to verify cache coherency protocols and other computer systems.[3]
The current system architecture, implemented in Nuprl 5, was first proposed in a 2000 conference paper. A reference manual for Nuprl 5 was published in 2002.[4] Nuprl has been the subject of many computer science publications.
Successors
[edit | edit source]Both the JonPRL and RedPRL systems are also based on computational type theory.[5] RedPRL is explicitly "inspired by Nuprl".[6]
References
[edit | edit source]- ^ a b Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
- ^ Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
- ^ Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
- ^ Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
- ^ Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
- ^ Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
External links
[edit | edit source]- PRL Project web page at Cornell University. The current maintainers of Nuprl have extensive documentation and publications on Nuprl.
- Former PRL Project web page at the Wayback Machine (archived November 14, 2023).
- A User-Level Introduction to the Nuprl Proof Development System (2001 paper at the University of Pennsylvania Scholarly Commons)
- RedPRL web page
Lua error in Module:Authority_control at line 153: attempt to index field 'wikibase' (a nil value).