Alternative definitions of the semantics:
- using inductive relations (as opposed to functional big-step style), and,
- as a small-step relation.
bigStepScript.sml: A clocked relational big-step semantics for CakeML. This semantics is no longer used in the CakeML development.
itree_semanticsScript.sml: An itree-based semantics for CakeML
proofs: The direcory contains proofs about the old relational semantics for CakeML. This directory might be deleted in the future.
smallStepScript.sml: A small-step semantics for CakeML. This semantics is no longer used in the main CakeML development, but is used in PureCake and choreographies.