An integration of HOL and ACL2

A link between the ACL2 and HOL4 proof assistants is described. This allows each system to be deployed smoothly within a single formal development. Several applications are being considered: using ACL2’s execution environment for simulating HOL models; using ACL2’s proof automa-tion to discharge HOL proof obligations; and using HOL to specify and verify properties of ACL2 functions that cannot easily be stated in the rst-order ACL2 logic. Care has been taken to ensure sound translations be-tween the logics supported by HOL and ACL2. The initial ACL2 theory has been dened inside HOL, so that it is pos-sible to prove mechanically that rst-order ACL2 functions on S-expressions correspond to higher-order functions op-erating on a variety of types. The translation between the two systems operates at the level of S-expressions and is in-tended to handle large hardware and software models. 1