Jason Hickey, Aleksey Nogin 
MetaPRL System Description

MetaPRL Editor Nuprl Type Theory Base Theory OCaml Syntax Tactic Mechanism Forward Chaining Distributed Proving Module Compiler Refiner MetaPRL Architecture MapMetaPRL is implemented as an extended OCaml compiler. Modules in MetaPRL can be plain programs, or they can be extended to additional logical definitions and syntax. The architecture of the system is summarized in the diagram at the right. The complete system contains these parts: