Nuprl System
Nuprl5
Nuprl 5 Reference Manual and User's Guide.
We also have an FAQ.
If you would like an account on our public server, please
email eaton@cs.cornell.edu with your ssh public key.
Downloadable Virtual Machines
By default Nuprl runs in the cloud.
Alternatively, one can run Nuprl locally using one of our virtual machines.
Nuprl in Coq
We've implemented and verified part of Nuprl in Coq.
More information can be found here.
EventML
EventML is a functional programming language with high level combinators that works with the Nuprl theorem prover
Formal Digital Library (FDL)
FDL (Formal Digital Library) was a generic name for Nuprl 5.
The FDL was intended to be a web service.
Nuprl 4
Nuprl 4 is no longer supported. If you have Nuprl 4 theories
which you would like migrated to Nuprl5, please send an email
to nuprl@cs.cornell.edu for assistance.
Nuprl4 shares many refiner and editor features with Nuprl5.
The Nuprl4 documentation may provide some information not yet
included in the nuprl5 docs.
Nuprl 4 User Documentation
MetaPRL (metaprl.org)
MetaPRL was designed and implemented by Jason Hickey as part of his PhD research. They system is described in detail in his PhD thesis and in several subsequent papers with users and collaborators. MetaPRL is a logical framework in the spirit of Isabelle and Twelf with the added capability of relating the logics. Jason first implemented the type theory of Nuprl, Computational Type Theory. MetaPRL is implemented in OCaml. Alexksey Nogin and Alexei Kopylov used MetaPRL extensively and contribute to its evolution. It is now used at Hughes Research Laboratory and at Moscow State University among other places. The MetaPRL system combines the properties of an interactive LCF-style tactic-based proof assistant, a logical framework, a logical programming environment, and a formal methods programming toolkit. MetaPRL is distributed under an open-source license and can be downloaded from http://metaprl.org/.
MetaPRL--A Modular Logical Environment
This paper provides an overview of the system focusing on the features that did not exist in the previous generations of PRL systems.