Jason Hickey, Aleksey Nogin, Alexei Kopylov 
MetaPRL User Guide

MetaPRL is implemented as an extension to the OCaml compiler. This document covers that language extension. To know more about the logical properties of MetaPRL, you should read about the logical framework, and to know more about the system implementation, you should read the system description.

The OCaml extension includes interfaces (.mli files), and implementations (.ml files). In OCaml, interfaces define module signatures: a declaration of the functions that comprise an implementation. In MetaPRL, we extend signatures with logical declarations: properties that are satisfied by the implementation, including properties about the ML programs in the implementation, and other logical properties including inference rules. The implementations contain programs that implement the ML declarations, and proofs that implement the logical part. The framework relies on the judgments-as-types principle: logical statements in an interface are types, and their proofs in the implementation are programs.

Unlike OCaml, the logical structure of a module is defined recursively by inheritance. The differences between the logical structure and the program structure are explained in the section on the extends directive.

The following sections describe each of the parts of the logical extension: