  This paper describes a C code generator for ACL2 that recognizes ACL2
representations of C constructs, according to a shallow embedding of C in ACL2,
and translates those representations to the represented C constructs. The code
generator also generates ACL2 theorems asserting the correctness of the C code
with respect to the ACL2 code. The code generator currently supports a limited
but growing subset of C that already suffices for some interesting programs.
This paper also offers a general perspective on language embedding and code
generation.
