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
cdr for creating
and manipulating list structures, various arithmetic primitives such
creating and manipulating symbols. Control primitives include
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
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.