Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP

Fetching latest commit…

Cannot retrieve the latest commit at this time

..
Failed to load latest commit information.
Holmakefile
README
bigSmallEquivScript.sml
bigSmallInvariants.lem
bigSmallInvariantsScript.sml
typeSoundInvariants.lem
typeSoundInvariantsScript.sml
typeSoundScript.sml
typeSysPropsScript.sml
untypedSafetyScript.sml
weakeningScript.sml

README

Theorems about the CakeML semantics.

The *.lem files are specified in Lem source
(http://www.cs.kent.ac.uk/~sao/lem/), and the corresponding *Script.sml files
are the HOL source generated from them by Lem.


bigSmallEquivScript.sml
    The equivalence between the big-step and small-step semantics

bigSmallInvariants.lem
    Definitions needed to state the invariants about big-step/small-step equivalence.
    Mostly, how to big-step evaluate intermediate small-step states.

evaluateEquationsScript.sml
    Some helper lemmas about the big-step relation.

typeSoundInvariants.lem
    Definitions needed to state the invariants about type soundness.  Mostly,
    how to type values and intermediate small-step states, and some
    well-formedness conditions on various type environments.

typeSoundScript.sml
    Type soundness.

typeSysPropsScript.sml
    Some useful lemmas about the type system.

untypedSafetyScript.sml
    Prove that for all programs, including ill-typed ones, the semantics never
    gets stuck, but instead raises Rtype_error.

weakeningScript.sml
    Weakening lemmas used in type soundness
Something went wrong with that request. Please try again.