[CakeML-dev] Greetings and my TFP'17 contribution

[Ramana Kumar]

Welcome Oskar!

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 :))

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.

Feel free to discuss further on or off list, as you prefer.

Cheers,
Ramana

On 16 May 2017 at 04:55, Oskar Abrahamsson <aboskar at chalmers.se> wrote:

> Greetings, CakeML developers.
>
> 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 :-)
>
> My thesis work concerns transforming certain recursive functions in the
> BVI part of the compiler into tail-recursive equivalents by introducing
> accumulator arguments (see https://github.com/CakeML/cakeml/issues/140).
> 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!
>
> I have attached the extended abstract as a PDF below.
>
> Regards,
> Oskar
>
>
> _______________________________________________
> Developers mailing list
> Developers at cakeml.org
> https://lists.cakeml.org/listinfo/developers
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/developers/attachments/20170516/0d5b2c16/attachment.html>