About-ACL2
General information About ACL2
This is ACL2 Version 8.6, copyright (C) 2025,
Regents of the University of Texas, authored by Matt Kaufmann and J Strother
Moore.
This manual contains
installation instructions,
tutorials,
and acknowledgments, as well as
information about mailing lists,
related publications, and ACL2 Workshops
.
See the ACL2 home
page for information about seminars and about other ACL2 releases.
See documentation for how to access the ACL2+Books User's
Manual.
For statistics on ACL2 code size, see file doc/acl2-code-size.txt.
Subtopics
- Recursion-and-induction
- Recursion and Induction
- Operational-semantics
- Modeling State Machines
- Soundness
- Correctness property claimed for ACL2
- Release-notes
- Pointers to what has changed
- Workshops
- The ACL2 Workshop Series.
- ACL2-tutorial
- Tutorial introduction to ACL2
- Version
- ACL2 Version Number
- Acknowledgments
- Some contributors to the well-being of ACL2
- Using-ACL2
- Using ACL2
- Releases
- ACL2 releases
- How-to-contribute
- Guide to contributing code to ACL2.
- Pre-built-binary-distributions
- Pre-built binary distributions of ACL2
- Common-lisp
- Relation to Common Lisp, including deviations from the spec
- Installation
- Installing ACL2
- Mailing-lists
- Mailing lists for ACL2 users
- Git-quick-start
- Git quick start guide.
- Copyright
- ACL2 copyright, license, authorship
- ACL2-help
- The acl2-help mailing list
