An Implementation of Higher Order Logic

We discuss a recent implementation of a mechanized proof assistant for the higher order logic known as HOL. We first describe high-level specification and proof facilities provided by the system, and then cover some details of the implementation. We explain how the module system of Standard ML provided security and modularity in the construction of the HOL kernel, as well as serving in a separate capacity as a useful representation medium for persistent, hierarchical logical theories.

paper