[CakeML] POPL'14 vs. ICFP'16

Lars Hupel hupel at in.tum.de
Tue Feb 7 18:34:56 UTC 2017


Hi,

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

Cheers
Lars

On 7 February 2017 17:45:02 CET, Yong Kiam <tanyongkiam at gmail.com> wrote:
>Hi Lars,
>
>There are equivalence proofs between the current functional <->
>relational
>big-step <-> small-step here:
>https://github.com/CakeML/cakeml/tree/master/semantics/alt_semantics
>
>There is an updated version of the semantics on a separate branch that
>uses
>Scott's new namespace theory:
>https://github.com/CakeML/cakeml/tree/env-refactor/semantics/alt_semantics
>
>We're working on getting that branch merged back into master.
>
>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).
>
>
>On Tue, Feb 7, 2017 at 11:17 AM, Lars Hupel <hupel at in.tum.de> wrote:
>
>> Dear CakeML developers,
>>
>> apart from the discussion of related work in the ICFP'16 paper, is
>there
>> any formal connection between the previous big-step semantics and
>> current functional semantics? I understand that you have extended the
>> source language significantly but was wondering whether there is any
>> equivalence proof of (possibly) a subset.
>>
>> Cheers
>> Lars
>>
>> _______________________________________________
>> Users mailing list
>> Users at cakeml.org
>> https://lists.cakeml.org/listinfo/users
>>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/users/attachments/20170207/a91f04a3/attachment.html>


More information about the Users mailing list