|
|
|---|
|
|
|
|---|
Libraries of ACL2 books developed by the ACL2 community.
This topic discusses ACL2 books, which are files of ACL2 events like definitions and theorems. See also community.
The ACL2 Community Books are the canonical set of open-source books for ACL2, developed since the early 1990s by members of the ACL2 community. They include libraries for reasoning in many domains, macro libraries for more quickly writing and documenting code, interfacing tools for connecting ACL2 to other systems, productivity tools for better proof automation and debugging, and specialty libraries for areas like hardware verification.
Most installations of ACL2 contain a copy of the Community Books. See installation.
Users are encouraged to contribute their own books. See how-to-contribute.
See community for more ways to become involved with the ACL2 community.