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.
- Error-checking
- A library of utilities for error checking.
- Apt
- APT (Automated Program Transformations) is a library of tools
to transform programs and program specifications
with automated support.
- Abnf
- A library for ABNF (Augmented Backus-Naur Form).
- 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.
- Prime-field-constraint-systems
- A library for PFCSes (Prime Field Constraint Systems).
- 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.
- 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.
- Java
- An ACL2 library for Java.
- C
- An ACL2 library for C.
- Syntheto
- An ACL2 library for the Syntheto language.
- Number-theory
- Some utilities related to number theory
- Cryptography
- A library for cryptography.
- Lists-light
- A lightweight library for lists.
- File-io-light
- A lightweight library for file input and output.
- Json
- A library for JSON.
- Built-ins
- A library about the ACL2 built-ins.
- Solidity
- An ACL2 library for Solidity.
- Axe
- The Axe toolkit
- Std-extensions
- Extensions of Std library in the Kestrel 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
