Making Induction Manifest in Modular ACL2

Date Added: Sep 2009
Format: PDF

ACL2, a Common Lisp-based language for programming and theorem proving, has enjoyed industrial success despite lacking modern language features such as a module system. In previous work, the authors equipped ACL2 with modules, interfaces, and explicit linking and measured their system with a series of experiments. One experiment revealed a serious lack of expressivity; the interfaces cannot describe the induction schemes necessary to reason about exported functions with nontrivial patterns of recursion. In this paper they revise their language, Modular ACL2, to overcome this weakness.