HOL is an abbreviation for Higher order logic, a branch of symbolic logic in which statements can be quantified over objects, predicates, predicates of predicates etc.

There is also a theorem prover called HOL; see HOL theorem prover.