 | |
| Paradigm | Functional, meta |
|---|---|
| Designed by | Robert S. Boyer, J Strother Moore and Matt Kaufmann |
| Developer | Matt Kaufmann and J Strother Moore |
| First appeared | 1990[1] (limited distribution), 1996 (public distribution) |
| Stable release | 8.6
/ October 2024 |
| Typing discipline | Dynamic |
| OS | Cross-platform |
| License | BSD |
| Website | www |
| Influenced by | |
| Common Lisp, Nqthm | |
Preview warning: Page using Template:Infobox programming language with unknown parameter "bodystyle"
ACL2 (A Computational Logic for Applicative Common Lisp) is a software system consisting of a programming language, an extensible theory in a first-order logic, and an automated theorem prover. ACL2 is designed to support automated reasoning in inductive logical theories, mostly for software and hardware verification. The input language and implementation of ACL2 are written in Common Lisp. ACL2 is free and open-source software.
- ^ "XDOC — Note-1-7". www.cs.utexas.edu.