<div dir="ltr"><div><div>Hi Lars,<br><br></div>There are equivalence proofs between the current functional <-> relational big-step <-> small-step here: <a href="https://github.com/CakeML/cakeml/tree/master/semantics/alt_semantics">https://github.com/CakeML/cakeml/tree/master/semantics/alt_semantics</a><br><br></div><div>There is an updated version of the semantics on a separate branch that uses Scott's new namespace theory: <a href="https://github.com/CakeML/cakeml/tree/env-refactor/semantics/alt_semantics">https://github.com/CakeML/cakeml/tree/env-refactor/semantics/alt_semantics</a><br><br></div><div>We're working on getting that branch merged back into master.<br><br>As far as I know, we don't strictly have what you are after, i.e. something that connects back to the original semantics as reported in POPL'14. Besides new operations, I think the main difference is the FFI oracle in the semantics. It might be possible to prove such a connection if those things were explicitly banned (Scott can probably answer this better).<br></div><div><br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Tue, Feb 7, 2017 at 11:17 AM, Lars Hupel <span dir="ltr"><<a href="mailto:hupel@in.tum.de" target="_blank">hupel@in.tum.de</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Dear CakeML developers,<br>
<br>
apart from the discussion of related work in the ICFP'16 paper, is there<br>
any formal connection between the previous big-step semantics and<br>
current functional semantics? I understand that you have extended the<br>
source language significantly but was wondering whether there is any<br>
equivalence proof of (possibly) a subset.<br>
<br>
Cheers<br>
Lars<br>
<br>
______________________________<wbr>_________________<br>
Users mailing list<br>
<a href="mailto:Users@cakeml.org">Users@cakeml.org</a><br>
<a href="https://lists.cakeml.org/listinfo/users" rel="noreferrer" target="_blank">https://lists.cakeml.org/<wbr>listinfo/users</a><br>
</blockquote></div><br></div>