NuPRL is a higher-order proof development system developed at Cornell University. It was founded by Joseph L. Bates and Robert L. Constable in 1979 and, since then, many have contributed to the development of NuPRL.
Nuprl is a computer system which provides assistance with logical problem solving. It supports the interactive creation of proofs, formulas, and terms in a formal theory of mathematics; with it one can express concepts associated with definitions, theorems, theories, books and libraries. Moreover, the theory is sensitive to the computational meaning of terms, assertions and proofs, and the system can carry out the actions used to define that computational meaning. Thus Nuprl includes a programming languages, but in a broader sense it is a system for implementing mathematics.
- Constable, Robert; Stuart F. Allen, H. M. Bromley, Walter Rance Cleaveland, J. F. Cremer, Robert W. Harper, Douglas J. Howe, Todd B. Knoblock, Nax P. Mendler, Prakash Panangaden, James T. Sasaki, and Scott F. Smith (1985). Implementing Mathematics with the Nuprl Development System. Prentice-Hall.
- Bickford, Mark; Robert L. Constable and Vincent Rahli (2012). "2012 Languages for Distributed Algorithms Workshop". Philadelphia.
|This logic-related article is a stub. You can help Wikipedia by expanding it.|
|This technology-related article is a stub. You can help Wikipedia by expanding it.|