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.