[CakeML-Dev] CF to translator

Armaël Guéneau armael.gueneau at ens-lyon.fr
Fri Oct 7 11:06:59 UTC 2016

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.

More information about the Developers mailing list