Systems in the HOL family use the ML programming language. This language was originally developed along with LCF to serve the purpose of a meta-language for theorem proving systems; in fact, the name stands for "Meta-Language".

*There should be information on the HOL logic here.*

There are four separate implementations of HOL. The first, HOL88, is the culmination of the original HOL implementation effort, led by Mike Gordon. It includes its own ML implementation, and is implemented on top of Common Lisp. The second, HOL90, uses Standard ML. The third, HOL98, uses Moscow ML. The current HOL 4 project is based on HOL98 and continues to use Moscow ML.

These three HOL implementations come with large libraries of theorem proving code. These implement extra automation on top of the very simple core code.

The fourth implementation, HOL Light, is much simpler than the others. It uses simpler axioms and inference rules to describe its logic (although the logic is essentially the same as other HOL implementations). It also has fewer libraries of automated tactics. HOL Light is implemented in CAML Light.

For more information about HOL, see " class="external">http://hol.sourceforge.net

HOL is a successor of the LCF theorem prover. Among the successors of HOL is the Isabelle theorem prover.