[CakeML] ML semantics

[Scott Owens]

If you’re generally interested in the small step semantics, it’s based on the CEK machine. We only used it for the type soundness proof because it was customary to do such proofs in the small-step setting (although usually for abstract machines with substitution rather than closures).

I’m currently working on making all of the system directly use the functional big step semantics — in the style of the ESOP ’16 paper — on the fbs-type-sound branch. Work is nearing completion and I hope to merge with master soon. We are keeping the relational big-step and the small-step semantics (and equivalence proofs) in an alt_semantics subdirectory, so that people who prefer to understand CakeML’s semantics with those still can, but I don’t plan to use them in our formal proofs.

Scott


> On 2016/07/25, at 21:30, Magnus Myreen <magnus.myreen at gmail.com> wrote:
> 
> I don't think it has been described in a paper with more than a line
> or two. The POPL'14 paper mentions the small-step semantics a few
> times: https://cakeml.org/popl14.pdf
> -- Magnus
> 
> On 25 July 2016 at 11:35, Gergely Buday <buday.gergely at uni-eszterhazy.hu> wrote:
>> Hi,
>> 
>> 
>> 
>> which paper describes the lem semantics of CakeML at
>> 
>> 
>> 
>> https://github.com/CakeML/cakeml/tree/master/semantics ?
>> 
>> 
>> 
>> https://cakeml.org/esop16.pdf
>> 
>> 
>> 
>> describes the big-step but there is a small-step semantics as well.
>> 
>> 
>> 
>> - Gergely
>> 
>> 
>> _______________________________________________
>> Users mailing list
>> Users at cakeml.org
>> https://lists.cakeml.org/listinfo/users
>> 
> 
> _______________________________________________
> Users mailing list
> Users at cakeml.org
> https://lists.cakeml.org/listinfo/users