HOL (
Higher Order Logic) denotes a family of
interactive theorem proving systems sharing similar
(higher-order) logics and implementation strategies. Systems in this family follow the
LCF approach as they are implemented as a library in some programming language. This library implements an
abstract data type of proven
theorems so that new objects of this type can only be created using the functions in the library which correspond to
inference rules in
higher-order logic. As long as these functions are correctly implemented, all theorems proven in the system must be valid. In this way, a large system can be built on top of a small trusted kernel.