<div dir="ltr"><div><div><div><div>Welcome Oskar!<br><br></div>I had a brief look at your paper draft. It's very good. I look forward to seeing your optimisations incorporated in CakeML (once the last few proofs are finished :))<br><br>One high-level comment is that you mention early on a few times (including in the abstract) that there are some surprising deficiencies in the verification technique used in many parts of the compiler proofs, but the explanation of this (in sec 4.2, I suppose) is not very clear. What's wrong with the techniques used and how can they be fixed? My understanding is that this has something to do with the fact that transformations that change evaluation order must be careful about whether subexpressions raise exceptions. I don't see how or what verification techniques you use are getting in the way of proving something that ought to be easier to prove, which is what I was hoping for when I read your abstract.<br><br></div>Feel free to discuss further on or off list, as you prefer.<br><br></div>Cheers,<br></div>Ramana<br></div><div class="gmail_extra"><br><div class="gmail_quote">On 16 May 2017 at 04:55, Oskar Abrahamsson <span dir="ltr"><<a href="mailto:aboskar@chalmers.se" target="_blank">aboskar@chalmers.se</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">



<div style="word-wrap:break-word">
Greetings, CakeML developers.
<div><br>
</div>
<div>I’ll start by introducing myself. My name is Oskar Abrahamsson, and for the past few months I have been working on additions to the CakeML compiler as my M.Sc. project at the CSE dept. at Chalmers, under the supervision of Magnus. Just recently,
 I was hired as a Ph.D. candidate at the same department, to be supervised by Magnus; so I’ll remain active in the project in the future as well :-)</div>
<div><br>
</div>
<div>My thesis work concerns transforming certain recursive functions in the BVI part of the compiler into tail-recursive equivalents by introducing accumulator arguments (see <a href="https://github.com/CakeML/cakeml/issues/140" target="_blank">https://github.com/<wbr>CakeML/cakeml/issues/140</a>).
 I have written up an extended abstract summarizing my work for the TFP’17 symposium, and Magnus suggested that I post it here for more feedback. The deadline is “Monday, 15 May, anywhere in the world”, so I’m a bit late, but I would be extremely grateful for
 any feedback — even if it’s past deadline!</div>
<div><br>
</div>
<div>I have attached the extended abstract as a PDF below.</div>
<div><br>
</div>
<div>Regards,</div>
<div>Oskar</div>
<div><br>
</div>
<div></div>
</div>

<br>______________________________<wbr>_________________<br>
Developers mailing list<br>
<a href="mailto:Developers@cakeml.org">Developers@cakeml.org</a><br>
<a href="https://lists.cakeml.org/listinfo/developers" rel="noreferrer" target="_blank">https://lists.cakeml.org/<wbr>listinfo/developers</a><br>
<br></blockquote></div><br></div>