An embedding of the ACL2 logic in HOL

Michael J. C. Gordon, Warren A. Hunt Jr., Matt Kaufmann, James Reynolds. An embedding of the ACL2 logic in HOL. In Panagiotis Manolios, Matthew Wilding, editors, Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2006, Seattle, Washington, USA, August 15-16, 2006. pages 40-46, ACM, 2006. [doi]

Abstract

Abstract is missing.