System
The current system is the FDL.
FDL
FDL is an acronym for Formal Digital Library. We use FDL as a more generic name for Nuprl 5.
We intend the FDL to be provided primarily as a web service.
As such if you would like acess to our public server, please
email eaton@cs.cornell.edu for assistance.
Nuprl 4
Nuprl 4 is no longer supported. If you have Nuprl 4 theories which you would like migrated to Nuprl5, please send email to eaton@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.
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 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.
|