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

May 24, 2022 · The Ethereal · 🏛 International Workshop on the ACL2 Theorem Prover and Its Applications

"No code URL or promise found in abstract"

Evidence collected by the PWNC Scanner

Authors Alessandro Coglio arXiv ID 2205.11708 Category cs.LO: Logic in CS Cross-listed cs.PL, cs.SE Citations 3 Venue International Workshop on the ACL2 Theorem Prover and Its Applications Last Checked 5 months ago

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.