"We include the necessary code to run J-Bob in ACL2 and Scheme, as well as a transcript of the proofs in the book. J-Bob is also included in the Dracula package for Racket."
Isn't ACL2 Common Lisp based? If it runs on Scheme/Racket and CL (or at least ACL2), it should be pretty easy to translate.
