MetaPRL System Description

MetaPRL is implemented as an extended OCaml compiler. Modules in MetaPRL can be plain prgrams, 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:

• The refiner implements logical operations and accounting. The refiner associates an accounting object called a sentinal with each module. The sentinal defines the valid set of logical inferences, syntax definitions, computational equaivalences, and programs in a module. The sentinal is passed between refiners during distributed computation to localize the context of a refinement.
• The module compiler is used to compile MetaPRL modules into two parts: an ML module that defines the computation in the module, and a sentinal that expresses the logical content. The module compiler is right above the refiner; it has no knowledge of proofs, whether they be automated or interactive. The compiler simply compiles logical content, to be used later by the module editor.
• The refiner defines an abstract logical interface. The distributed prover implements the same interface, but the logical operations are spread across multiple machines. The distributed prover contains a scheduler to hand out logical goals, and a failure recovery algorithm to handle refiner failures.
• The forward chainer implements proof caching and forward chaining. Currently, forward chaining is restricted to forward rules with a finite forward closure. Once again, the forward chainer reimplements the refiner interface.
• The tactic definitions implement the tactic combinator language over the refiner. Logical proofs use basic combinators: each logical definition in a module defines a tactic, and the tactic module provide tactic combinators that are used for automation.
• The OCaml syntax is defined as a logical module containing syntax definitions and an operational semantics for the OCaml definitions in a module. The module compiler compiles ML programs to logical terms; the OCaml syntax module defines the logical properties and semantics of the programs.
• The logic definition module defines properties shared by many logics. For example, the MetaPRL framework has no knowledge of sequents, but many logics use sequents to express their inference rules. The basic logic module defines sequents. In addition, the basic logic module defines tactics for automation, including automation of introduction and elimination rules, equality reasoning, and general tactic-based search.
• The logics currently defined include the Nuprl type theory, Aczel's set theory, first order logic, and a partial implementation of the Edinburgh logical framework (LF).
• The module editor provides interactive support, including a module navigator, a proof editor, and context-sensitive toploop language.