		Search-engine friendly clone of the ACL2 documentation.

Pub-papers

Pub-foundations

Foundations

CS313K Notes, J Strother Moore, University of Texas at Austin, 2024
Integrating External Deduction Tools with ACL2, Matt Kaufmann, J S. Moore, Sandip Ray, and Erik Reeber. Journal of Applied Logic (Special Issue: Empirically Successful Computerized Reasoning), Volume 7, Issue 1, March 2009, pp. 3--25. Published online, DOI 10.1016/j.jal.2007.07.002. Preliminary version in C. Benzmueller, B. Fischer, and G. Sutcliffe (eds.), Proceedings of the 6th International Workshop on the Implementation of Logics (IWIL 2006), Phnom Penh, Cambodia, November 2006, pages 7-26. Volume 212 of CEUR Workshop Proceedings.
An Integration of HOL and ACL2, Michael J.C. Gordon, Warren A. Hunt, Jr., Matt Kaufmann, and James Reynolds. In Proceedings of Formal Methods in Computer-Aided Design (FMCAD'06) (A. Gupta and P. Manolios, eds.). IEEE Computer Society Press, pp. 153-160, November, 2006. Slides are available here.
See also: An Embedding of the ACL2 Logic in HOL, Michael J.C. Gordon, Warren A. Hunt, Jr., Matt Kaufmann, and James Reynolds. In P. Manolios and M. Wilding (eds.), Proceedings of the 6th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2006), Seattle, WA, August 2006, pages 40-46. Proceeding have also been published in the ACM Digital Library. Copyright ACL2 Steering Committee.
Integrating CCG analysis into ACL2, Matt Kaufmann, Panagiotis Manolios, J Moore, and Daron Vroon). Proceedings of The Eighth International Workshop on Termination (WST 2006), August, 2006.
Quantification in Tail-recursive Function Definitions, Sandip Ray. In P. Manolios and M. Wilding (eds.), Proceedings of the 6th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2006), Seattle, WA, August 2006, pages 95-98. Proceeding have also been published in the ACM Digital Library. Copyright ACL2 Steering Committee.
Adding a Total Order to ACL2, M. Kaufmann and P. Manolios. In Proceedings of ACL2 Workshop 2002.
Single-Threaded Objects in ACL2, Robert Boyer and J Moore. Single-threaded objects in ACL2 are structures that have the normal “copy-on-write” applicative semantics one expects in a functional programming language but which are implemented by destructive modification. The axiomatic “story” is consistent with the implementation because syntactic restrictions are enforced which insure that only the modified structure is subsequently referenced. Single-threaded objects (or “stobjs”) are particularly useful in modeling microprocessors, where the state of the processor is modeled as a stobj.
Structured Theory Development for a Mechanized Logic, M. Kaufmann and J Moore, Journal of Automated Reasoning 26, no. 2 (2001), pp. 161-203. This paper presents a precise development of the encapsulate and include-book features of ACL2 and gives careful proofs of the high-level correctness properties of these ACL2 structuring mechanisms.
A Precise Description of the ACL2 Logic, Matt Kaufmann and J Moore, April, 1998. This paper is a working draft of a precise description of the base logic. The draft does not describe the theorem prover or the system; it is a dry mathematical document describing the logic from first principles. At the moment the description omits encapsulation, multiple values, property lists, arrays, state, and macros.
The ACL2 User's Manual. Originally written by Matt Kaufmann and J Moore, it now includes contributions from ACL2 users, in particular to document many ACL2 books. The user's manual is a vast hypertext document.