Skip to main content
PRL Project

Nuprl System


Nuprl 5 Reference Manual and User's Guide.
We also have an FAQ.
If you would like an accound on our public server, please email 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 is a functional programming language with high level combinators that works with the Nuprl theorem prover

Downloads and Documentation

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 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 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

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.