[Axiom-developer] GCL and LLVM

[daly]

Camm,

I've begun working on proving an Axiom algorithm. I'm looking
at Coq to work the proof at the Spad level and ACL2 to work the
proof at the Lisp level.

Hardin, et.al [Hard14] has published a paper on an LLVM-to-ACL2
translator. Since GCL generates C, this looks like a way to
bridge the proof from Lisp to the hardware.

So, the question is, have you tried hosting GCL on LLVM?

Tim

[Hard14] Hardin, David S.; Davis, Jennifer, A.; Greve, David A.;
         McClurg, Jedidiah R.
``Development of a Translator from LLVM to ACL2''
http://arxiv.org/pdf/1406.1566