An Integration of HOL and ACL2

We describe a link between the ACL2 and HOL mechanical proof assistants that enables the strengths of each system to be deployed smoothly within a single formal development. Several application scenarios are being considered: using ACL2's high performance execution environment by converting HOL models into ACL2; using ACL2's proof automation to discharge HOL proof obligations; and importing ACL2 definitions and theorems into HOL, to specify and verify properties that cannot easily be stated in the first-order ACL2 logic. Particular 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 higherorder functions operating on a variety of types. The translation between the two systems operates at the level of S-expressions, and has been engineered to allow large models to be converted...

• Type: Conference
• Year: 2006
• Where: FMCAD
• Authors: Michael J. C. Gordon, James Reynolds, Warren A. Hunt Jr., Matt Kaufmann
• Keywords: ACL2, First-order Acl2, FMCAD 2006, Formal Methods, Initial Acl2 Theory