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 type theory contains
*untyped*programs, and*types*that are used to state propositions and classify the programs. - The type theory is
*predicative*(there are no non-trivial types that contain themselves), and it is*higher-order*. - Types are expressive, there are:
- Type
*universes*that contain types, - Function types
`A -> B`, dependent function type whose range depends on the argument`(x: 'A -> 'B['x])`, and very-dependent function types (`{ f | x: 'A -> 'B['f; 'x] }`), whose range depends on the argument, and the function itself. - Product types
`'A * 'B`, representing pairs of values, and dependent product types (`x: 'A * 'B['x]`), representing pairs whose`snd`type depends on the`fst`element. - Recursive types
`mu{x. 'T['x]}` - Types that eliminate computation, including
- The
*"set"*type`{ x: 'A | 'B['x] }` - Union types
`union x: 'A. 'B['x]` - Intersection types
`isect x: 'A. 'B['x]`

- The
- Quotient types
`x, y: 'A // 'P['x; 'y]`, that modify type equality.

- Type

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