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. See also http://www.cs.cmu.edu/Web/Groups/AI/html/cltl/cltl2.html.
ACL2 formalizes only a subset of Common Lisp. It includes such familiar Lisp
functions as cons, car and cdr for creating and manipulating list
structures, various arithmetic primitives such as +, *, expt and
<=, and intern and symbol-name for creating and manipulating
symbols. Control primitives include cond, case and if, as well
as function call, including recursion. New functions are defined with
defun and macros with defmacro. See programming 
for a list
of the Common Lisp primitives supported by ACL2.
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)
* conses
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, f(x) must be equal to f(x), which
means, among other things, that the value of f must not be affected by
``global variables'' and the object x must not change over time.
