Nuprl

Last updated

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.

Contents

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.

Successors

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

Related Research Articles

Automated theorem proving is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a major impetus for the development of computer science.

<span class="mw-page-title-main">Software</span> Non-tangible executable component of a computer

Software is a collection of programs and data that tell a computer how to perform specific tasks. Software often includes associated software documentation. This is in contrast to hardware, from which the system is built and which actually performs the work.

In mathematics and theoretical computer science, a type theory is the formal presentation of a specific type system. Type theory is the academic study of type systems.

Computer science is the study of the theoretical foundations of information and computation and their implementation and application in computer systems. One well known subject classification system for computer science is the ACM Computing Classification System devised by the Association for Computing Machinery.

In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of a system with respect to a certain formal specification or property, using formal methods of mathematics. Formal verification is a key incentive for formal specification of systems, and is at the core of formal methods. It represents an important dimension of analysis and verification in electronic design automation and is one approach to software verification. The use of formal verification enables the highest Evaluation Assurance Level (EAL7) in the framework of common criteria for computer security certification.

<span class="mw-page-title-main">Theoretical computer science</span> Subfield of computer science and mathematics

Theoretical computer science (TCS) is a subset of general computer science and mathematics that focuses on mathematical aspects of computer science such as the theory of computation, formal language theory, the lambda calculus and type theory.

Intuitionistic type theory is a type theory and an alternative foundation of mathematics. Intuitionistic type theory was created by Per Martin-Löf, a Swedish mathematician and philosopher, who first published it in 1972. There are multiple versions of the type theory: Martin-Löf proposed both intensional and extensional variants of the theory and early impredicative versions, shown to be inconsistent by Girard's paradox, gave way to predicative versions. However, all versions keep the core design of constructive logic using dependent types.

Question answering (QA) is a computer science discipline within the fields of information retrieval and natural language processing (NLP) that is concerned with building systems that automatically answer questions that are posed by humans in a natural language.

Axiom is a free, general-purpose computer algebra system. It consists of an interpreter environment, a compiler and a library, which defines a strongly typed hierarchy.

<span class="mw-page-title-main">Logic in computer science</span> Academic discipline

Logic in computer science covers the overlap between the field of logic and that of computer science. The topic can essentially be divided into three main areas:

<span class="mw-page-title-main">Proof assistant</span> Software tool to assist with the development of formal proofs by human-machine collaboration

In computer science and mathematical logic, a proof assistant or interactive theorem prover is a software tool to assist with the development of formal proofs by human-machine collaboration. This involves some sort of interactive proof editor, or other interface, with which a human can guide the search for proofs, the details of which are stored in, and some steps provided by, a computer.

<span class="mw-page-title-main">Programming language theory</span> Branch of computer science

Programming language theory (PLT) is a branch of computer science that deals with the design, implementation, analysis, characterization, and classification of formal languages known as programming languages. Programming language theory is closely related to other fields including mathematics, software engineering, and linguistics. There are a number of academic conferences and journals in the area.

Metamath is a formal language and an associated computer program for archiving and verifying mathematical proofs. Several databases of proved theorems have been developed using Metamath covering standard results in logic, set theory, number theory, algebra, topology and analysis, among others.

Robert Lee Constable is an American computer scientist. He is a professor of computer science and first and former dean of the Faculty of Computing and Information Science at Cornell University. He is known for his work on connecting computer programs and mathematical proofs, especially the Nuprl system. Prior to Nuprl, he worked on the PL/CV formal system and verifier. Alonzo Church was supervising the junior thesis of Robert while he was studying in Princeton. Constable received his PhD in 1968 under Stephen Kleene and has supervised over 40 students, including Edmund M. Clarke, Robert Harper, Kurt Mehlhorn, Steven Muchnick, Pavel Naumov, and Ryan Stansifer. He is a Fellow of the Association for Computing Machinery.

In the field of type theory in computer science, a quotient type is a data type which respects a user-defined equality relation. A quotient type defines an equivalence relation on elements of the type - for example, we might say that two values of the type Person are equivalent if they have the same name; formally p1 == p2 if p1.name == p2.name. In type theories which allow quotient types, an additional requirement is made that all operations must respect the equivalence between elements. For example, if f is a function on values of type Person, it must be the case that for two Persons p1 and p2, if p1 == p2 then f(p1) == f(p2).

<span class="mw-page-title-main">Prakash Panangaden</span> American/Canadian computer scientist

Prakash Panangaden is an American/Canadian computer scientist noted for his research in programming language theory, concurrency theory, Markov processes and duality theory. Earlier he worked on quantum field theory in curved space-time and radiation from black holes. He is the founding Chair of the ACM Special Interest Group on Logic and Computation.

This glossary of computer science is a list of definitions of terms and concepts used in computer science, its sub-disciplines, and related fields, including terms relevant to software, data science, and computer programming.

Lean is a proof assistant and programming language. It is based on the calculus of constructions with inductive types. It is an open-source project hosted on GitHub. It was principally developed by Leonardo de Moura while employed by Microsoft Research and now Amazon Web Services, and has had significant contributions from other coauthors and collaborators during its history.

References

  1. 1 2 "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. ↑ Harper, Robert; Angiuli, Carlo (May 10, 2017). "Computational higher-dimensional type theory" (PDF). 43nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL).
  7. ↑ "The People's Refinement Logic". www.redprl.org. Retrieved 2017-10-24.
This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.