ACL2

ACL2
ParadigmFunctional, meta
Designed byRobert S. Boyer, J Strother Moore and Matt Kaufmann
DeveloperMatt Kaufmann and J Strother Moore
First appeared1990[1] (limited distribution), 1996 (public distribution)
Stable release
8.6 / October 2024 (2024-10)
Typing disciplineDynamic
OSCross-platform
LicenseBSD
Websitewww.cs.utexas.edu/users/moore/acl2
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.

  1. ^ "XDOC — Note-1-7". www.cs.utexas.edu.