论文标题
基于ACL2中C的浅嵌入ACL2的证明生成C代码生成器
A Proof-Generating C Code Generator for ACL2 Based on a Shallow Embedding of C in ACL2
论文作者
论文摘要
本文介绍了ACL2的C代码生成器，该生成器识别C构建体的ACL2表示，根据C中C的浅嵌入ACL2，并将这些表示形式转换为代表的C构建体。代码生成器还生成了ACL2定理，主张相对于ACL2代码的C代码的正确性。代码生成器当前支持C的有限但增长的C子集，该子集已经足以容纳一些有趣的程序。本文还提供了有关语言嵌入和代码生成的一般视角。
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.
