We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs.LO

Change to browse by:

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Logic in Computer Science

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

Authors: Alessandro Coglio (Kestrel Institute)
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.
Comments: In Proceedings ACL2 2022, arXiv:2205.11103
Subjects: Logic in Computer Science (cs.LO); Programming Languages (cs.PL); Software Engineering (cs.SE)
Journal reference: EPTCS 359, 2022, pp. 185-201
DOI: 10.4204/EPTCS.359.15
Cite as: arXiv:2205.11708 [cs.LO]
  (or arXiv:2205.11708v1 [cs.LO] for this version)

Submission history

From: EPTCS [view email]
[v1] Tue, 24 May 2022 01:19:06 GMT (24kb,D)

Link back to: arXiv, form interface, contact.