TY  - RPRT
TI  - A Proof-Generating C Code Generator for ACL2 Based on a Shallow Embedding of C in ACL2
AU  - Alessandro Coglio
PY  - 2022
DO  - 10.4204/eptcs.359.15
UR  - https://arxiv.org/abs/2205.11708
ID  - 2205.11708
ER  -