The direcory contains proofs about the old relational semantics for CakeML. This directory might be deleted in the future.
alt_semanticsScript.sml: Relate top-level semantics for function big-step / relational big-step / small-step semantics.
bigClockScript.sml: Theorems about the clocked big-step semantics. Primarily that they are total, and that they have the proper relationship to the unclocked version.
bigSmallEquivScript.sml: Big step/small step equivalence
bigSmallInvariantsScript.sml: Invariants used in the proof relating the big-step and small-step version of the CakeML source semantics.
bigStepPropsScript.sml: A few properties about the relational big-step semantics.
determScript.sml: Determinism for the small-step and relational big-step semantics
funBigStepEquivScript.sml: Relate functional big-step semantics with relational big-step semantics.
interpComputeLib.sml: Compset for evaluating the functional big-step semantics.
interpScript.sml: Deriviation of a functional big-step semantics from the relational one.
itree_semanticsEquivScript.sml: Relating the itree- and FFI state-based CakeML semantics
itree_semanticsPropsScript.sml: Properties about the itree- and FFI state-based CakeML semantics
smallStepPropsScript.sml: Properties about the small-step semantics.