<div dir="ltr"><div><div>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.<br>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.)<br>Armaël, perhaps you could look at writing the automation to do CF -> translator and translator -> CF based on the theorem I proved?<br></div>Magnus, when you get a chance, look at the last cheat left for you?<br></div>Everything is currently in cfAppScript.sml, but I'll move things back into the semantics/proofs and translator/ directories when I get a chance.<br></div><div class="gmail_extra"><br><div class="gmail_quote">On 8 October 2016 at 22:24, Ramana Kumar <span dir="ltr"><<a href="mailto:Ramana.Kumar@cl.cam.ac.uk" target="_blank">Ramana.Kumar@cl.cam.ac.uk</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><span class=""><blockquote style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex" class="gmail_quote">I'm happy to make a minor tweak to the definition of st2heap and prove<br>
the following. I would appreciate help with proving lemma 2 from the<br>
following.</blockquote><div class="gmail_extra"><br></div></span><div class="gmail_extra">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).<br></div><div><div class="h5"><div class="gmail_extra"><br><div class="gmail_quote">On 7 October 2016 at 22:06, Armaël Guéneau <span dir="ltr"><<a href="mailto:armael.gueneau@ens-lyon.fr" target="_blank">armael.gueneau@ens-lyon.fr</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span><br>
<br>
On 07/10/2016 12:39, Magnus Myreen wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Excellent!<br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
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:<br>
1. Does the final theorem look like a strong enough connection?<br>
</blockquote>
Probably yes. I think Armaël might know better than me.<br>
</blockquote></span>
Yes, I think it's strong enough.<br>
<br>
</blockquote></div><br></div></div></div></div>
</blockquote></div><br></div>