HOL is an acronym for Higher Order Logic. It is an environment written in the programming language ML which allows for interactive theorem proving.