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

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 "distributed open architecture"[1] and intended primarily to be used as a web service rather than as standalone software. Those interested in using the web service, or migrating theories from older versions of Nuprl, can contact the email address given on the Nuprl System web page.[2]

History

Nuprl was first released in 1984, and was first described in detail in the book Implementing Mathematics with the Nuprl Proof Development System,[3] 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.[4]

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.[5] Nuprl has been the subject of many computer science publications, some as recent as 2014.[6]

Successors

Both the JonPRL and RedPRL systems are also based on computational type theory.[7] RedPRL is explicitly "inspired by Nuprl".[8]

gollark: - It's important to me that women aren't forced to have children they don't want or may not be able to take care of.- which is why I support mandatory sterilization for all - children would be grown in vats and raised by the government instead.
gollark: - I support the right to privacy!- In light of governments' large-scale mass surveillance campaigns which they do not seem inclined to stop, I would support an open and transparent volunteer spying agency using open source software and hardware to gather and process data in order to act as a competitor.
gollark: These are hard...
gollark: - which is why I think all government workers should be randomly selected, similarly to jury duty
gollark: - which is why I think anyone in government who makes a mistake of any kind should be immediately fired

References
  1. "Nuprl 5 distributed open architecture". PRL Project. Retrieved 7 March 2015.
  2. "Nuprl System". PRL Project. Retrieved 7 March 2015.
  3. Constable, Robert; et al. (1986). Implementing Mathematics with The Nuprl Proof Development System. Englewood Cliffs, NJ: Prentice-Hall. ISBN 1468059106. Retrieved 7 March 2015.
  4. Allen, Stuart; Constable, Robert; Eaton, Richard; Kreitz, Christoph; Lorigo, Lori. "The Nuprl Open Logical Environment (2000 slide presentation)" (PDF). Retrieved 7 March 2015.
  5. Kreitz, Christoph (2002). The Nuprl Proof Development System, Version 5: Reference Manual and User’s Guide (PDF).
  6. "PRL Project - Knowledge Base". PRL Project. Retrieved 7 March 2015.
  7. Harper, Robert; Angiuli, Carlo (May 10, 2017). "Computational higher-dimensional type theory" (PDF). 43nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL).
  8. "The People's Refinement Logic". www.redprl.org. Retrieved 2017-10-24.
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.