The ACL2 community:
ACL2 Community Books.
See URL https://code.google.com/p/acl2-books/.
Shilpi Goel, Warren A. Hunt, Jr. & Matt Kaufmann (2013):
Abstract Stobjs and Their Application to ISA Modeling.
In: Proceedings 11th International Workshop on the ACL2 Theorem Prover and its Applications.
Matt Kaufmann & J Strother Moore:
ACL2 documentation topic: RELEASE-NOTES.
See URL http://www.cs.utexas.edu/users/moore/acl2/current/RELEASE-NOTES.html.
Matt Kaufmann & J Strother Moore:
Instructions for modifying ACL2 system code.
See URL http://www.cs.utexas.edu/users/moore/acl2/open-architecture/how-to-make-patches.txt.
Matt Kaufmann & J Strother Moore (2011):
How Can I Do That with ACL2? Recent Enhancements to ACL2.
In: David Hardin & Julien Schmaltz: ACL2,
EPTCS 70,
pp. 46–60.
Available at http://dx.doi.org/10.4204/EPTCS.70.4.
Guy L. Steele, Jr. (1990):
Common LISP: the language (2nd ed.).
Digital Press,
Newton, MA, USA.