# ACL2-programming-language

A library about the ACL2 programming language.

The ACL2 theorem prover includes a programming language,
which is essentially a subset of Common Lisp.
ACL2 also includes a logical language,
which is a superset of a subset of Common Lisp.

This library formalizes certain aspects of
the syntax and semantics of
the ACL2 programming language.

The formalization of the ACL2 evaluation semantics in this library
is currently just the work of this library's author.
It is not an official descripion of the ACL2 evaluation semantics
in an analogous sense that this techical report is an official description of the ACL2 logical semantics.
Refer to manual pages like this one for an official description of the ACL2 evaluation semantics.

### Subtopics

- Primitive-functions
- A formalization of the ACL2 primitive functions.
- Translated-terms
- A formalization of ACL2 translated terms.
- Values
- A formalization of ACL2 values.
- Evaluation
- Evaluation.
- Program-equivalence
- Program equivalence.
- Functions
- A formalization of ACL2 defined functions.
- Packages
- A formalization of ACL2 packages.
- Programs
- A formalization of ACL2 programs.
- Interpreter
- A program-mode interpreter.
- Evaluation-states
- Evaluation states.