Kestrel-books
A collection of ACL2 books contributed mainly by Kestrel Institute.
The Kestrel Books are a collection of ACL2 books
contributed mainly by Kestrel Institute. The Kestrel Books are freely available under a liberal license.
Specific copyright, author, and license information
is provided in the individual files and subdirectories.
As they become more stable,
parts of the Kestrel Books may be moved
to other locations in the Community Books. For example, STD and X86ISA include some Kestrel contributions.
Many of the Kestrel Books build upon,
and are meant to extend and be compatible with,
the ACL2 system code
and various existing libraries such as STD, FTY, Seq, and others.
Subtopics
- Crypto-hdwallet
- A hierarchical deterministic wallet for cryptocurrencies.
- Apt
- APT (Automated Program Transformations) is a library of tools
to transform programs and program specifications
with automated support.
- Error-checking
- A library of utilities for error checking.
- Fty-extensions
- Extensions of FTY in the Kestrel Books.
- Isar
- An ACL2 library for Isar-style proofs.
- Kestrel-utilities
- Utilities that are part of the
Kestrel Books.
- Soft
- SOFT (Second-Order Functions and Theorems)
is a tool to mimic second-order functions and theorems
in the first-order logic of ACL2.
- Bv
- The BV library for reasoning about bit-vectors
- Imp-language
- An ACL2 library for the simple programming language Imp.
- Event-macros
- A library of concepts and utilities for event macros.
- C
- An ACL2 library for C.
- Java
- An ACL2 library for Java.
- Bitcoin
- A library for Bitcoin.
- Ethereum
- A library for Ethereum.
- Yul
- An ACL2 library for Yul.
- Zcash
- A library for Zcash.
- ACL2-programming-language
- A library about the ACL2 programming language.
- Prime-fields
- A library about prime fields.
- Json
- A library for JSON.
- Syntheto
- An ACL2 library for the Syntheto language.
- File-io-light
- A lightweight library for file input and output.
- Number-theory
- Some utilities related to number theory
- Cryptography
- A library for cryptography.
- Lists-light
- A lightweight library for lists.
- Builtins
- A library about the ACL2 built-ins.
- Axe
- The Axe toolkit
- Solidity
- An ACL2 library for Solidity.
- Helpers
- Tools for finding, improving, and repairing proofs and books.
- Htclient
- HTTP/HTTPS client library
- Typed-lists-light
- A lightweight library for lists of items of various types.
- Arithmetic-light
- An arithmetic library developed using a lightweight approach
