A Simple Java Code Generator for ACL2 Based on a Deep Embedding of ACL2 in Java

TL;DR

This paper introduces AIJ, a deep Java embedding of a subset of ACL2, and ATJ, a Java code generator that translates ACL2 functions into AIJ for execution and interoperability with Java, simplifying integration and verification.

Contribution

It presents a straightforward Java code generator for ACL2 based on a deep embedding, enabling easier execution and integration of ACL2 code within Java environments.

Findings

AIJ allows ACL2 code to run as Java code without Lisp runtime.

ATJ translates ACL2 functions into AIJ representations for evaluation.

The generated Java code's performance may be sufficient for some applications.

Abstract

AIJ (ACL2 In Java) is a deep embedding in Java of an executable, side-effect-free, non-stobj-accessing subset of the ACL2 language without guards. ATJ (ACL2 To Java) is a simple Java code generator that turns ACL2 functions into AIJ representations that are evaluated by the AIJ interpreter. AIJ and ATJ enable possibly verified ACL2 code to run as, and interoperate with, Java code, without much of the ACL2 framework or any of the Lisp runtime. The current speed of the resulting Java code may be adequate to some applications.