research
∙
05/24/2022
A Proof-Generating C Code Generator for ACL2 Based on a Shallow Embedding of C in ACL2
This paper describes a C code generator for ACL2 that recognizes ACL2 re...
share
research
∙
05/24/2022
A Complex Java Code Generator for ACL2 Based on a Shallow Embedding of ACL2 in Java
This paper describes a code generator that translates ACL2 constructs to...
research
∙
05/24/2022
Syntheto: A Surface Language for APT and ACL2
Syntheto is a surface language for carrying out formally verified progra...
research
∙
09/29/2020
Isomorphic Data Type Transformations
In stepwise derivations of programs from specifications, data type refin...
research
∙
09/29/2020
Ethereum's Recursive Length Prefix in ACL2
Recursive Length Prefix (RLP) is used to encode a wide variety of data i...
research
∙
10/10/2018
Adding 32-bit Mode to the ACL2 Model of the x86 ISA
The ACL2 model of the x86 Instruction Set Architecture was built for the...
research
∙
10/10/2018
A Simple Java Code Generator for ACL2 Based on a Deep Embedding of ACL2 in Java
AIJ (ACL2 In Java) is a deep embedding in Java of an executable, side-ef...
research
∙
05/03/2017