AIJ (ACL2 In Java) is a deep embedding of ACL2 in Java.
AIJ is a deep embedding in Java of an executable, side-effect-free, non-stobj-accessing subset of the ACL2 language without guards.
AIJ is realized as a Java package that includes Java representations of all the ACL2 values, Java implementations of all the ACL2 primitive functions, and an interpreter that evaluates ACL2 translated terms to ACL2 values. The interpreter evaluates terms ``in the logic'', without checking guards and without side effects. The interpreter evaluates if non-strictly. The interpreter can be invoked only on (Java representations of) concrete ACL2 values, not on global variables like state and user-defined stobjs.
AIJ is in the
The Java source files of AIJ may be edited either in IntelliJ IDEA
or in a text editor like Emacs.
These source files can be compiled either in IntelliJ IDEA
or via the
AIJ is written in Java 8,
which means that it can be compiled
using a compiler for Java 8 or later.