9 citations · 43 across the 13 of their papers we have counts for
Showing 2022Show all
3 papers · 1 filter
cs.LO2022★ 4 cited
A Proof-Generating C Code Generator for ACL2 Based on a Shallow Embedding of C in ACL2
Alessandro Coglio
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 represent…
cs.LO2022★ 2 cited
A Complex Java Code Generator for ACL2 Based on a Shallow Embedding of ACL2 in Java
Alessandro Coglio
This paper describes a code generator that translates ACL2 constructs to corresponding Java constructs, according to a shallow embedding of ACL2 in Java. Starting from purely funct…
cs.SE2022
Syntheto: A Surface Language for APT and ACL2
Alessandro Coglio, Eric McCarthy, Stephen Westfold +3
Syntheto is a surface language for carrying out formally verified program synthesis by transformational refinement in ACL2 using the APT toolkit. Syntheto aims at providing more fa…