|
|
|---|
|
|
|
|---|
Shallow embedding of C in ACL2 for ATC.
We are in the process of moving this shallow embedding
from the
The ACL2 representation of C constructs, which ATC recognizes and translates to C, constitutes a shallow embedding of C in ACL2. In contrast, the abstract syntax, static semantics, and dynamic semantics constitute a deep embedding of C in ACL2. The two are separate but related of course, via the theorems generated by ATC, which are in fact more general than ATC in a way, because they are applicable to code lifting besides code generation.
The file where this XDOC topic appears can be included by tools, such as APT transformations, that need to operate on the ACL2 representations of the C constructs, without having to include all of ATC.