## Functions for Manipulating these Objects

Consider a typical ``stack'' of control frames.

Suppose the model required that we express the idea of ``the most recent
frame whose return program counter points into `MAIN`

.''

The natural expression of this notion involves

**function application** -- ``fetch the `return-pc`

of this frame''

**case analysis** -- ``**if** the pc is `MAIN`

, **then** ...''

**iteration** or **recursion** -- ``pop this frame off and repeat.''

The designers of ACL2 have taken the position that a **programming**
**language** is the natural language in which to define such notions,
**provided** the language has a mathematical foundation so that models can be
analyzed and properties derived logically.

Common Lisp is the language supported by ACL2. To be precise, a small
applicative subset of Common Lisp is the language supported by ACL2.