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 automation to discharge HOL proof obligations; and using HOL to specify and verify properties of ACL2 functions that cannot easily be stated in the first-order ACL2 logic. Care has been taken to ensure sound translations between the logics supported by HOL and ACL2. The initial ACL2 theory has been defined inside HOL, so that it is possible to prove mechanically that first-order ACL2 functions on S-expressions correspond to higher-order functions operating on a variety of types. The translation between the two systems operates at the level of S-expressions and is intended to handle large hardware and software models