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

TL;DR

This paper presents a C code generator for ACL2 that recognizes C constructs within ACL2 representations, translates them into C, and generates theorems to verify correctness, supporting a subset of C for practical programs.

Contribution

It introduces a novel shallow embedding of C in ACL2 and a code generator that produces verified C code from ACL2 representations.

Findings

Supports a subset of C sufficient for interesting programs

Generates ACL2 theorems for code correctness

Provides insights on language embedding and code generation

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.