
<html><head></head><body>Hi,<br>

<br>

thanks for the pointer, that looks exactly like what I was looking for.<br>

<br>

Cheers<br>

Lars<br><br><div class="gmail_quote">On 7 February 2017 17:45:02 CET, Yong Kiam <tanyongkiam@gmail.com> wrote:<blockquote class="gmail_quote" style="margin: 0pt 0pt 0pt 0.8ex; border-left: 1px solid rgb(204, 204, 204); padding-left: 1ex;">

<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>

</blockquote></div></body></html>