Re: [Gcl-devel] GCL and LLVM

[Camm Maguire]

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,

address@hidden 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                                        address@hidden
==========================================================================
"The earth is but one country, and mankind its citizens."  --  Baha'u'llah