Intuitionistic Type Theory

The module ITT is the largest, and most complete, logic in MetaPRL. The paper Formal Abstract Data Types gives an explanation of the logic. The logic can be summarized as follows:

The following diagram illustrates the inheritance hierarchy in the type theory.

ITT hierarchy