Abstract

The ACL2 theorem prover provides formal reasoning tools for a pure, first-order subset of Common Lisp. Companies such as AMD, IBM, and Rockwell Collins use ACL2 to model and verify critical hardware and software artifacts. Unfortunately, ACL2 is a small, simple language, while the models it verifies are large and complex. ACL2 has a few tools up its sleeve to tame this complexity: macros, packages, and encapsulation. Unfortunately, these tools each come with their own pitfalls. Unhygienic macros are a metaprogramming tool that is oblivious to the scope of names. Common Lisp’s package system provides namespace management in a way that causes more problems than it solves. And ACL2’s encapsulation mechanism defines logical abstractions that prevent a model from being executed, are cumbersome to instantiate, and tend to increase code duplication rather than decreasing it.

For my PhD dissertation, I designed and implemented a language called “Refined ACL2” that resolves these problems by equipping the logic and core language of ACL2 with the hygienic macros of Racket and the module system of ML. Racket’s hygienic macros observe lexical scope, allowing complex language extensions while avoiding pitfalls such as unintended capture. The ML module system provides both namespace management and logical abstraction, without the difficulties of Common Lisp’s packages, and while remaining both executable and easy to instantiate.