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 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.
Click here for a simple example of Common Lisp.
