Formal module systems

The logical environment organizes the contents of the logical library using theory modularity, as we discussed in Section . The formal module system we propose provides the features of standard programming modules, promoted to the formal domain based on the mathematical practice of the last century.

Within this module system, the root of a mathematical theory is defined as a module containing the fundamental definitions of the theory, and formal features are defined in submodules that are based on the formal definitions. For instance, the module structure of the Nuprl type theory is shown in Figure 2.

  

Figure 2: Modular design of the Nuprl type theory

The root theory in the Figure is a module that defines only the most fundamental features of Nuprl: the typing and equality judgments. The modules below the root define the properties of each of its type constructors: function and product spaces, disjoint unions, etc. Finally, the constructive Nuprl theory joins the common constructors together to form the computational Nuprl type theory.

Most of the current knowledge in Nuprl is expressed in the standard Nuprl theory. The classical Nuprl theory is obtained by adding the choice operator. The framework allows the classical theory to inherit all the results of the constructive theory.