[CakeML] Low-level Compiler Explorer
Ramana.Kumar at cl.cam.ac.uk
Wed Jul 23 13:20:09 UTC 2014
On Wed, Jul 23, 2014 at 1:59 PM, Lars Hupel <hupel at in.tum.de> wrote:
> Right, exactly. I used Lem to generate Isabelle theories from the
> "semantics" folder in the "vml" repository. I made some preliminary
> experiments and was already able to prove some trivial lemmas for
> evaluation of arithmetic expressions with no toplevel definitions involved.
> My long-term goal is to write a compiler from Isabelle code equations to
> CakeML ASTs (via a deeply-embedded term rewriting fragment of HOL as an
> intermediate step).
> (This is obviously inspired from the ICFP'12 paper by Myreen and Owens.)
Apart from the ICFP'12 paper, there is an updated JFP paper available from
the authors' websites (Magnus, Scott, we should link to this from cakeml.org
And for the ground truth, there is the code (maybe even with some limited
comments and README) in the "translator" folder of the CakeML code
I imagine both the code and the journal paper will be useful in porting the
translator to Isabelle. I'd be very interested to see your progress on
this, and of course am happy to help where I can.
> > Yes it is possible. At the moment the numerous ways I can think of
> > such output involve running HOL4. If you are not opposed to that, I can
> > spell them out. (Also, if it's a one-off thing, you can just send me the
> > code and I can send back the AST.)
> Yes, I'd appreciate that.
I guess one place to start could be
translator/ml_translator_demoScript.sml, and also the
> I'm already in the process of trying to build a repository snapshot of
> HOL4 with Poly/ML, but so far am struggling with some linker issues.
> I'll report back if I can't get it to work.
The people on (and archives of) the hol-info mailing list (see
http://hol.sf.net) may be of help.
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Users