Sciweavers

FMCAD
2006
Springer

An Integration of HOL and ACL2

14 years 4 months ago
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...
Michael J. C. Gordon, James Reynolds, Warren A. Hu
Added 22 Aug 2010
Updated 22 Aug 2010
Type Conference
Year 2006
Where FMCAD
Authors Michael J. C. Gordon, James Reynolds, Warren A. Hunt Jr., Matt Kaufmann
Comments (0)