[CakeML-Dev] CF to translator

Ramana Kumar Ramana.Kumar at cl.cam.ac.uk
Sat Oct 8 11:24:28 UTC 2016


>
> 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/20161008/802ed4e1/attachment.html>


More information about the Developers mailing list