From Wikipedia, the free encyclopedia
Jump to: navigation, search

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.[1]

Nuprl's logic is a constructive type theory called Computational Type Theory (CTT). It allows users to reason about events including protocols for distributed computing.[2]


  1. ^ 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. 
  2. ^ Bickford, Mark; Robert L. Constable and Vincent Rahli (2012). "2012 Languages for Distributed Algorithms Workshop". Philadelphia.  |chapter= ignored (help)

External links[edit]