A Proof-Generating C Code Generator for ACL2 Based on a Shallow Embedding of C in ACL2

Abstract

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.

In Proceedings ACL2 2022, arXiv:2205.11103

References in corpus (2)

• Mechanized semantics for the Clight subset of the C language
• A Complex Java Code Generator for ACL2 Based on a Shallow Embedding of ACL2 in Java

Cited by in corpus (1)

• A Complex Java Code Generator for ACL2 Based on a Shallow Embedding of ACL2 in Java