Reflection with the implementation language

In any formal framework, the language used for proof automation provides a key link between logic and knowledge. Proof automation is used to rephrase the fundamental mathematics into proof intuitive procedures specific to mathematical domains.

Our approach in Nuprl-Light integrates the formal module system with the OCaml programming language modules, providing a form of reflection in the system. We can use the formal system to speak about its implementation. The formal effect of this reflection is to add a new semantics of ML to the module structure. For our work in Nuprl, a formal interpretation of the OCaml semantics is given in Nuprl, allowing Nuprl to be used to reason about OCaml programs. At the programming level, the effect is to augment OCaml modules with formal statements.

In practice, there are two types of modules--those the define the type theory, and those that define ML programs. For instance, the module in Figure 4 defines a partial description of the Nuprl logical implication.

  

Figure 4: Implication module fragment

This module is derived from the root Nuprl module NuprlRootSig, and it defines a new syntax for a type constructor $A \Rightarrow B$. The final axiom statement defines the propositional behavior of implication: $A \Rightarrow B$ is true if whenever A is true, then B is true.

The module construction for reasoning about programs has a similar layout. The module in Figure 5 is used to define nonempty sets of numbers. This module uses the Nuprl interpretation of OCaml (defined in NuprlSig) and it defines a type t to represent non-empty sets with three operators: singleton creates a set with one element, union combines two sets, and mem tests for set membership. Finally, the remaining two statements give the formal verification properties for the set: the singleton set really contains one element, and the union contains exactly the elements in the sets being combined.

 

Figure:   module