[CakeML-Dev] CF to translator
armael.gueneau at ens-lyon.fr
Fri Oct 7 11:06:59 UTC 2016
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.
More information about the Developers