R-and-i-annotated-bibliography
Recursion and Induction: Annotated Bibliography
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 microprocessor 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 superseded 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).
Table of Contents
