Recursion and Induction: Annotated Bibliography

The following resources are useful for understanding the ACL2 logic and theorem prover, as well as its relation to both the earlier Nqthm logic and the Common Lisp programming language. These resources are not necessary for you to do the exercises in these notes. But if you are considering learning how to use the ACL2 or just wondering why anyone would bother, you might browse this annotated bibliography.

- [0] R. S. Boyer and J S. Moore.

*A Computational Logic Handbook*.

Academic Press, London, 1997 (Second Edition).

See*https://www.cs.utexas.edu/users/boyer/ftp/nqthm/*

for source code and regression suite

This book is the user's manual for the Boyer-Moore theorem prover, Nqthm, of the 1980s. The ACL2 project started in 1989, when Boyer and Moore set themselves the goal of re-implementing Nqthm so that it supported an efficient, functional (applicative) subset of Common Lisp and was coded in that same subset. (They almost succeeded but had to use imperative code to implement functional versions of some utilities.) So this reference, [0], describes the precursor of ACL2. This book is the second edition of the Nqthm manual which was first published in 1988. The url above contains the Nqthm source code and input and output files for the prover. Most of these files were developed by the Nqthm user community. The files include many proofs of classic list-processing and elementary number theory theorems but also proofs of Goedel's incompleteness theorem, Gauss's law of quadratic reciprocity, the Paris-Harrington Ramsey theorem, and the “verified stack” of Computational Logic, Inc. The verified stack, first reported in 1989 and then ported to a verified fabricated microprocessor in 1992, consisted of a gate-level implementation of a microprocessor, an assembler, linker, and loader, a compiler, an operating system, and some applications, all of which were verified with Nqthm to “stack” so that a theorem proved about an application written in one of two high level languages and proved correct with respect to that high-level semantics runs correctly on the microprocessor. These results are only briefly mentioned in [0] but that book does contain citations that describe them in detail. Further development of Nqthm was halted because Nqthm users were building formal models that were so big they strained the capacity of the prover and were too slow to run as simulators for the modeled systems. For example, when the ACL2 project was getting started, a student of Boyer was formalizing the Motorola 68020 micrprocessor with the goal of verifying the Berkeley C String Library. (That Nqthm project was completed successfully in 1993 and the files are available at the url above.) - [1] M. Kaufmann, P. Manolios, and J S. Moore, editors.

*Computer-Aided Reasoning: ACL2 Case Studies*.

Kluwer Academic Press, Boston, MA., 2000.

See*https://www.cs.utexas.edu/users/moore/publications/acl2-books/acs/index.html*.

This book is a collection of papers by ACL2 users, assembled in 2000, describing, in a textbook-like style. applications of ACL2. It contains examples from graph theory, calculus, model checking, language simulators, microprocessor design including hardware description languages, floating-point implementations, compiler verification, and other topics. While the Kluwer hardback edition of the book is out of print, the url above includes instructions for obtaining a paperback copy (for which the authors of [1] and [2] hold the copyright). - [2] M. Kaufmann, P. Manolios, and J S. Moore.

*Computer-Aided Reasoning: An Approach*.

Kluwer Academic Press, Boston, MA., 2000.

*https://www.cs.utexas.edu/users/moore/publications/acl2-books/car/index.html*.

This book is essentially a textbook for students wishing to learn how to use the ACL2 system. It starts with a description of the ACL2 programming language, then formalizes the logic with axioms and rules of inference, and then discusses how to prove theorems with the system. The book includes exercises. While the Kluwer hardback edition of the book is out of print, the url above includes instructions for obtaining a paperback copy (for which the authors of [1] and [2] hold the copyright). - [3] M. Kaufmann and J S. Moore.

A precise description of the ACL2 logic.

In*https://www.cs.utexas.edu/users/moore/publications/km97a.pdf*

Dept. of Computer Science, University of Texas at Austin, 1997.

The title says it all. The ACL2 logic is a first-order logic of total recursive functions providing mathematical induction and several extension principles including symbol package definition and recursive function definition. The logic is a formalization of an extension of a functional subset of Common Lisp. This paper describes the logic in detail, more in the style of a logic book than the style used in these notes. The paper also explains the connection between theorems in the logic and evaluation in Common Lisp, which very roughly speaking is that, given enough time and computing resources, any instance of a guard-verified (aka a “gold” theorem in the terminology of this 1997 paper) will compute to non-nil in Common Lisp. (Maybe explore <<`verify-guards`>>?) - [4] M. Kaufmann and J S. Moore.

The ACL2 home page.

*http://www.cs.utexas.edu/users/moore/acl2/*

Dept. of Computer Science, University of Texas at Austin, 2022.

This web page contains the latest release of the ACL2 system in Common Lisp source code form. The system is largely implemented in the subset of Common Lisp the prover supports. ACL2 is distributed without fee under a 3-clause BSD license. A new release is currently made about once per year and the web page also contains links to all past releases going back to 1996. The home page includes instructions for installing any of several Common Lisp implementations and instructions for downloading and building ACL2. The web page contains the online user's manual and instructions for how to download the regression suite from the ACL2 GitHub repository. The regression suite, called the ACL2 <<Community-Books>>, contains thousands of verified files created by the ACL2 user community containing definitions and theorems. If you scan down to the**Subtopics**section of the <<top>> node of the manual you will find a list of many topics for which certified <<books>> are available. To take just one example from that top-level list of Subtopics, scroll down to Hardware Verification. In that Subtopic you find directories dealing with symbolic simulation, register transfer logic (including tools for reasoning about floating point implementations), a Verilog translator, an x86 ISA model, and many other topics. There are many other nodes besides Hardware Verification. In fact, the tree of books listed among the Subtopics is simply too big and too rapidly changing to try to summarize here. We encourage you to explore, or ask <<ACL2-help>> about resources (if any) for a particular topic. - [5] P. Manolios and D. Vroon.

Ordinal arithmetic in acl2.

In*ACL2 Workshop 2003*, Boulder, Colorado, July 2003.

http://www.cs.utexas.edu/users/moore/acl2/workshop-2003/.

The termination of recursive functions in ACL2 and the induction principle are both based on the ordinals and the well-foundedness of ordinal “less than”. The description of ACL2 in [2] above includes a formalization of the ordinals up to ε_0 (“epsilon naught”) represented in ACL2 with conses and natural numbers based on a version of Cantor Normal Form. That representation was superceded in 2004 by the representation described in this paper, which implements a slightly different version of the normal form that is exponentially more efficient. The paper also describes algorithms for manipulating ordinals in this representation. - [6] K. Pitman (editor).

*Common Lisp Hyper Spec*.

LispWorks, Ltd, 1996.

http://www.lispworks.com/documentation/HyperSpec/Front/.

This is an online hypertext presentation of the Common Lisp specification as described in [7]. - [7] G. L. Steele, Jr.

*Common Lisp The Language, Second Edition*.

Digital Press, 30 North Avenue, Burlington, MA. 01803, 1990.

This is the definitive specification of Common Lisp. ACL2 only formalizes a small subset of the language described by Steele. But ACL2's documentation of some primitives refers to Steele's descriptions. By the way, we do not recommend the ACL2 documentation as a way to learn to how to program in full Common Lisp. Indeed, we don't recommend [6] or [7] for that purpose either. Many good introductions to Common Lisp are available via the web. There are many implementations of Common Lisp available and the installation instructions on the ACL2 home page list several. - [8] W. A. Hunt, Jr., M. Kaufmann, J S. Moore and A. Slobodova.

Industrial Hardware and Software Verification with ACL2.

In*Verified Trustworthy Software Systems*, P. Gardner, P. O'Hearn, M. Gordon,

G. Morrisett and F. B. Schneider, Phil. Trans. R. Soc. A,**375**, The Royal Society,

ISSN 1364-503X, DOI 10.1098/rsta.2015.0399 (Article Number 20150399), 2017.

The ACL2 system has seen sustained industrial use since the mid-1990s. Companies that have used ACL2 regularly include AMD, Centaur Technology, IBM, Intel, Kestrel Institute, Motorola/Freescale, Oracle and Collins (formerly Rockwell Collins). This paper describes how ACL2 came to be used in industry, what it is used for, and how it is used. The paper highlights ACL2's use in the microprocessor industry, specifically by Centaur Technology on modules in their x86 microprocessors. The paper was written in 2017. Since then the formal verification team at Centaur Technology has moved to Intel, where ACL2 is used in the same way today (2022).