[CakeML-Dev] CF to translator
Ramana.Kumar at cl.cam.ac.uk
Sun Oct 9 00:17:20 UTC 2016
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
> 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>
>> On 07/10/2016 12:39, Magnus Myreen wrote:
>>> 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...
More information about the Developers