A Thread of HOL Development
The HOL system is a mechanized proof assistant for higher order
logic that has been under continuous development since the mid-1980s,
by an ever-changing group of developers and external contributors. We
give a brief overview of various implementations of the HOL logic
before focusing on the evolution of certain important features
available in a recent implementation. We also illustrate 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