The logic of ACL2 is based on Common Lisp.
Common Lisp is the standard list processing programming language. It is documented in: Guy L. Steele, Common Lisp The Language, Digital Press, 12 Crosby Drive, Bedford, MA 01730, 1990.
ACL2 formalizes only a subset of Common Lisp. It includes such familiar
Lisp functions as
ACL2 supports five of Common Lisp's datatypes:
* the precisely represented, unbounded numbers (integers, rationals, and the complex numbers with rational components, called the ``complex rationals'' here),
* the characters with ASCII codes between 0 and 255
* strings of such characters
* symbols (including packages)
ACL2 is a very small subset of full Common Lisp. ACL2 does not include the
Common Lisp Object System (CLOS), higher order functions, circular structures,
and other aspects of Common Lisp that are non-applicative. Roughly
speaking, a language is applicative if it follows the rules of function
application. For example,