Modular proof development in ACL2

• Online Access: http://hdl.handle.net/2047/d20002853

The ACL2 theorem prover combines a first-order dialect of LISP with an automated proof engine for first-order logic. While ACL2 is logically quite powerful, it can be difficult to build and maintain large models due to its ad hoc systems for modularity, namespace management, logical encapsulation, and macro expansion. I propose a new language, Refined ACL2, extending ACL2 with expressive component and macro systems designed to accommodate large-scale proof development and flexible logical abstractions. The component system of Refined ACL2 adapts many features of ML's functors and signatures to ACL2. Components support nesting, parameterization, translucent specification, and refinement of abstract specifications with concrete definitions. Refined ACL2 inherits Racket's macro system; furthermore, macro definitions can be incorporated into component specifications.