Greetings! I had looked briefly at having gcl compile to the gcc intermediate form, and ship it as a gcc front end, but did not get very far. As I understand that LLVM also interfaces with gcc here, this would likely be the path to an llvm connection. But it seems this should not stand in the way of your project, as both LLVM and GCL (and hence acl2) have C as a common target.
BTW, is there a stable axiom release past 20120501 that I should package for Debian? Take care, d...@axiom-developer.org writes: > 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 > > > > > -- Camm Maguire c...@maguirefamily.org ========================================================================== "The earth is but one country, and mankind its citizens." -- Baha'u'llah _______________________________________________ Gcl-devel mailing list Gcl-devel@gnu.org https://lists.gnu.org/mailman/listinfo/gcl-devel
