NuPRL

From Wikipedia, the free encyclopedia

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]

References

  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. ↑ "The Logic of Events, a framework to reason about distributed systems". 2012 Languages for Distributed Algorithms Workshop. Philadelphia. 2012.  Unknown parameter |Last= ignored (|last= suggested) (help); Unknown parameter |First= ignored (|first= suggested) (help); |coauthors= requires |author= (help)

External links


This article is issued from Wikipedia. The text is available under the Creative Commons Attribution/Share Alike; additional terms may apply for the media files.