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