HOL: A Proof Generating System for Higher-Order Logic

HOL is a version of Robin Milner’s LCF theorem proving system for higher-order logic. It is currently being used to investigate (1) how various levels of hardware behaviour can be rigorously modelled and (2) how the resulting behavioral representations can be the basis for verification by mechanized formal proof. This paper starts with a tutorial introduction to the meta-language ML. The version of higher-order logic implemented in the HOL system is then described. This is followed by an introduction to goal-directed proof with tactics and tacticals. Finally, there is a little example of the system in action which illustrates how HOL can be used for hardware verification.