ACL2 To Java

Team:

• Alessandro Coglio (Lead)
• Limei Gilham
• Christoph Kreitz
• Eric Smith
• Stephen Westfold

We are building ATJ (= ACL2 To Java), a Java code generator for the ACL2 theorem prover. ATJ translates ACL2 code to Java, using specific Java constructs if the ACL2 code has a specific form.

ATJ complements APT. These two tools provide a way to synthesize Java code from high-level specifications, with proofs reaching the lowest-level ACL2 code just before Java code generation. We plan to extend ATJ to generate proofs of correctness of the Java code with respect to the ACL2 code, similarly to ATC.

ATJ is available here and documented here.

Also see ATC, a C code generator for ACL2.

Publications

A Simple Java Code Generator for ACL2 Based on a Deep Embedding of ACL2 in Java
Alessandro Coglio
November 2018
15th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2-2018)

A Complex Java Code Generator for ACL2 Based on a Shallow Embedding of ACL2 in Java
Alessandro Coglio
May 2022
17th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2-2022)