MetaPRL is part of a suite of projects under the heading Nuprl. The Nuprl projects are managed by Robert Constable, the Nuprl page gives the history and scope of the Nuprl work. MetaPRL was conceived in January 1996 to address the concerns of scalability in formal systems. In the early part of the decade, Nuprl formalizations were mostly limited to smaller problems that focused on basic data structures and mathematical foundations. As the foundations were implemented, it became possible to formalize larger problems, like the verification of Ensemble being performed by Kreitz, Hayden, and Hickey. As with any growing system, scalability became a major concern: how do we share our results with other systems; how do we design domain-specific logics; how do we get the computational speed for proving properties of large systems? These questions led to the modular design on MetaPRL, where logical theories are treated as formal objects that include both the logical knowledge and domain-specific heuristics needed to use that knowledge.
Jason Hickey is the main author and architect of MetaPRL. The system is a large part of his PhD thesis "Frameworks for sharing mathematics and programming." (This will be placed online sometime in the Fall '98).
Alexey Nogin is also a major contributor to MetaPRL. His implementations of the core data structures in MetaPRL have led to dramatic speedups in logical speed (over two orders of magnitude on some problems).
Eli Barzilay is working on proof structures for MetaPRL. His work is leading to proof representations that address the problem of fragility that all tactic-based provers share.