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
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 is no longer supported. If you have Nuprl 4 theories
which you would like migrated to Nuprl5, please send an email
to firstname.lastname@example.org 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 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.