[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Gcl-devel] GCL and LLVM
From: |
daly |
Subject: |
[Gcl-devel] GCL and LLVM |
Date: |
Sat, 14 Jun 2014 18:27:04 -0500 |
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
- [Gcl-devel] GCL and LLVM,
daly <=