ACL2 is an Untyped Language
The example
ACL2 !>(app '(a b c) 27)
(A B C . 27)
illustrates the fact that ACL2's logic is untyped (click here
for a brief discussion of the typed versus untyped nature of the logic).
The definition of app makes no restriction of the arguments to lists.
The definition says that if the first argument satisfies endp 
then return the second argument. In this example, when app has recursed
three times down the cdr of its first argument, '(a b c), it
reaches the final nil, which satisfies endp, and so 27 is returned.
It is naturally consed into the emerging list as the function returns from
successive recursive calls (since cons does not require its arguments
to be lists, either). The result is an ``improper'' list, (a b c . 27).
You can think of (app x y) as building a binary tree by replacing
the right-most tip of the tree x with the tree y.
