[CakeML-Dev] CF to translator

[Ramana Kumar]

Working on the translator-cf-basic branch, I've proved the connection
between Arrow and app_basic modulo the one cheat Magnus said he would prove.
My next step is to try to update the translator with the new Eval and Arrow
definitions. (So I might be moving definitions and theorems around, into
the appropriate files, but I might not get to this until tomorrow.)
Armaël, perhaps you could look at writing the automation to do CF ->
translator and translator -> CF based on the theorem I proved?
Magnus, when you get a chance, look at the last cheat left for you?
Everything is currently in cfAppScript.sml, but I'll move things back into
the semantics/proofs and translator/ directories when I get a chance.

On 8 October 2016 at 22:24, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk> wrote:

> I'm happy to make a minor tweak to the definition of st2heap and prove
>> the following. I would appreciate help with proving lemma 2 from the
>> following.
>
>
> No problem. I've replaced my cheated lemma 2 by the one you said you'd
> provide (i.e. I proved what I need from that).
>
> On 7 October 2016 at 22:06, Armaël Guéneau <armael.gueneau at ens-lyon.fr>
> wrote:
>
>>
>>
>> On 07/10/2016 12:39, Magnus Myreen wrote:
>>
>>> Excellent!
>>>
>>> I have proved the following connection between CF's app_basic (as on
>>>> master) and a revised formulation of the translator's Arrow, modulo 4
>>>> cheats. In this email, I will show: the final theorem proved, the cheated
>>>> lemmas, and the new Arrow definition. I ask for the following feedback:
>>>> 1. Does the final theorem look like a strong enough connection?
>>>>
>>> Probably yes. I think Armaël might know better than me.
>>>
>> Yes, I think it's strong enough.
>>
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/developers/attachments/20161009/e36db3ba/attachment.html>