Nuprl is a proof development system, providing computer-mediated analysis andproofs of formal mathematical statements, and tools forsoftware verification and optimization. Originally developed in the 1980s byRobert Lee Constable and others, the system is now maintained by the PRL Project atCornell University. The currently supported version, Nuprl 5, is also known as FDL (Formal Digital Library). Nuprl functions as anautomated theorem proving system and can also be used to provideproof assistance.
Nuprl uses atype system based onMartin-Löfintuitionistic type theory to model mathematical statements in adigital library. Mathematical theories can be constructed and analyzed with a variety of editors, including agraphical user interface, a web-based editor, and anEmacs mode. A variety of evaluators and inference engines can operate on the statements in the library. Translators also allow statements to be manipulated withJava andOCaml programs.[1] The overall system is controlled with a variant ofML.
Nuprl 5's architecture is described as "distributedopen architecture"[1] and intended primarily to be used as aweb service rather than as standalone software. Those interested in using the web service, or migrating theories from older versions of Nuprl, can contact theemail address given on the Nuprl System web page.[2]
Nuprl was first released in 1984, and was first described in detail in the bookImplementing Mathematics with the Nuprl Proof Development System,[3] published in 1986. Nuprl 2 was the firstUnix version. Nuprl 3 provided machine proof for mathematical problems related toGirard's paradox andHigman's lemma. Nuprl 4, the first version developed for theWorld Wide Web, was used to verify cache coherency protocols and other computer systems.[4]
The current system architecture, implemented in Nuprl 5, was first proposed in a 2000conference paper. A reference manual for Nuprl 5 was published in 2002.[5] Nuprl has been the subject of manycomputer science publications.
Both theJonPRL andRedPRL systems are also based on computational type theory.[6] RedPRL is explicitly "inspired by Nuprl".[7]
