ACL2, aka A Computational Logic for Applicative Common Lisp, is an open source programming language created in 1990 by Robert S. Boyer and J Strother Moore.

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 the purpose of software and hardware verification. The input language and implementation of ACL2 are built on Common Lisp. Read more on Wikipedia...

• ACL2 Wikipedia page
• ACL2 first developed in The University of Texas at Austin
• Explore ACL2 snippets on Rosetta Code
• ACL2 on HOPL
• See also: (2 related languages)Common Lisp, AXIOM