Toward a Practical Module System for ACL2

Abstract. Boyer and Moore's ACL2 theorem prover combines firstorder applicative Common Lisp with a computational, first-order logic. While ACL2 has become popular and is being used for large programs, ACL2 forces programmers to rely on manually maintained protocols for managing modularity. In this paper, we present a prototype of Modular ACL2. The system extends ACL2 with a simple, but pragmatic func

• Type: Conference
• Year: 2009
• Where: PADL
• Authors: Carl Eastlund, Matthias Felleisen
• Keywords: Applicative Common Lisp, Modular ACL2, PADL 2009, Programming Languages, Theorem Prover Combines