[CakeML] Low-level Compiler Explorer

[Ramana Kumar]

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.
>

Cool!


> 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
too, no?).

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
repository.

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
> getting
> > 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
ml_translatorLib.hol2deep function.


> 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.


>
> Cheers
> Lars
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/users/attachments/20140723/51401a1b/attachment.html>