[CakeML] POPL'14 vs. ICFP'16

[Yong Kiam]

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/7971d5e2/attachment.html>