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.
A Simple Java Code Generator for ACL2 Based on a Deep Embedding of ACL2 in Java
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
17th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2-2022)