The semantics of CakeML

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.

lib.lem
    Setup some HOL library in Lem, and define environments and lookup.

lexer_funScript.sml
    A functional specification of a lexing from strings to token lists.

tokens.lem
    The tokens.

tokenUtilsScript.sml
    Some theorems about tokens that the grammar needs.

gramScript.sml
    The grammar that specifies how token lists should be converted to concrete
    syntax trees

cmlPtreeConversionScript.sml
    Functions to convert the concrete syntax tree into a parsing AST. Removes
    some syntactic sugar.

ast.lem
    Defines the AST.

typeSystem.lem
    Specifies the type system.

semanticPrimitives.lem
    Definitions of semantic primitives (e.g., values, and functions for doing
    primitive operations) that are use in both the big-step and small-step
    semantics.

smallStep.lem
    A small-step semantics based on the CEKS machine. Only for expressions.

bigStep.lem
    A big-step semantics.  For modules, definitions, and expressions.
    The big-step and small-step semantics are proven equivalent in the
    metatheory directory.

funBigStep.lem
    A clocked functional version of the big-step semantics. (This version will
    eventually be used as the main semantics.)

terminationScript.sml
    Termination proofs for recursive functions defined in the .lem files.

initialProgram.lem
    CakeML ASTs that define the initial basis environment.

printScript.sml
    Specifies printing of results.

replScript.sml
    Pulls everything together into a semantics for the CakeML REPL.

standaloneScript.sml
    Pulls everything together into a semantics for whole CakeML programs.

proofs/
    Proofs of basic properties of the semantics, including determinism and a
    clocked interpreter.