<div dir="ltr"><div class="gmail_extra"><div class="gmail_quote">On Wed, Jul 23, 2014 at 1:59 PM, Lars Hupel <span dir="ltr"><<a href="mailto:hupel@in.tum.de" target="_blank">hupel@in.tum.de</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">

Right, exactly. I used Lem to generate Isabelle theories from the<br>
"semantics" folder in the "vml" repository. I made some preliminary<br>
experiments and was already able to prove some trivial lemmas for<br>
evaluation of arithmetic expressions with no toplevel definitions involved.<br></blockquote><div><br></div><div>Cool!<br></div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">

My
long-term goal is to write a compiler from Isabelle code equations to<br>
CakeML ASTs (via a deeply-embedded term rewriting fragment of HOL as an<br>
intermediate step).<br>

(This is obviously inspired from the ICFP'12 paper by Myreen and Owens.)<br></blockquote><div><br></div><div>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 <a href="http://cakeml.org">cakeml.org</a> too, no?).<br>

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

</div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div class="">
> Yes it is possible. At the moment the numerous ways I can think of getting<br>
> such output involve running HOL4. If you are not opposed to that, I can<br>
> spell them out. (Also, if it's a one-off thing, you can just send me the<br>
> code and I can send back the AST.)<br>
<br>
</div>Yes, I'd appreciate that.<br></blockquote><div><br></div><div>I guess one place to start could be translator/ml_translator_demoScript.sml, and also the ml_translatorLib.hol2deep function.<br></div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">



I'm already in the process of trying to build a repository snapshot of<br>
HOL4 with Poly/ML, but so far am struggling with some linker issues.<br>
I'll report back if I can't get it to work.<br></blockquote><div><br></div><div>The people on (and archives of) the hol-info mailing list (see <a href="http://hol.sf.net">http://hol.sf.net</a>) may be of help.<br>

</div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<br>
Cheers<br>
<span class="HOEnZb"><font color="#888888">Lars<br>
</font></span></blockquote></div><br></div></div>