The CakeML project (https://cakeml.org).

A verified implementation of a significant subset of Standard ML in the HOL4
theorem prover (http://hol-theorem-prover.org).

We build CakeML using the latest development version of HOL4.
We build HOL on PolyML 5.6 (http://www.polyml.org).
Example build instructions can be found in build-instructions.sh.

This branch (master) contains the latest development version of CakeML.
See the version1 branch for the previous version.

Directory structure:

- semantics
    The definition of CakeML, including
    - its concrete syntax
    - its abstract syntax
    - small step semantics
    - big step semantics (both functional and relational)
    - semantics of FFI calls
    - a type system
    The definition is (mostly) expressed in
    Lem (http://www.cs.kent.ac.uk/~sao/lem),
    but the generated HOL is also included.

- semantics/proofs
    Metatheory of CakeML and other proofs about the semantics
    - a verified, clocked interpreter
    - determinism
    - type soundness
    - equivalence of the big and small step semantics
    - equivalence of functional and relational semantics

- compiler
    A verified compiler for CakeML, including:
    - parsing: lexer and PEG parser
    - inference: type inferencer
    - backend: compilation to ASM assembly language
    - targets: code generation to x86, ARM, and more

- translator
    A proof-producing translator from HOL functions to CakeML.

- candle
    Verification of a HOL theorem prover, based on HOL Light
    (http://www.cl.cam.ac.uk/~jrh13/hol-light/), implemented in CakeML.

- unverified/front-end
    Stale unverified implementation, in Haskell, of the CakeML frontend
    augmented with informative error messages.
- unverified/ocaml-syntax
    A translator from OCaml to CakeML
- unverified/hol-light-syntax
    Another translator from OCaml to CakeML, targetted at translating HOL Light
- unverified/reg_alloc
    An implementation of CakeML's (verified) register allocator in Standard ML,
    used for a translation-validation based optimisation for evaluating the
    compiler in the logic.
- unverified/benchmarks
    Some ML benchmarks

- explorer
    Tools for stepping through execution of the compiler from one intermediate
    language to the next, and pretty-printing the intermediate results. An
    instance is available on the CakeML website.

- mlstringScript.sml, mlstringLib.sml, mlstringSyntax.sml
    Small theory of wrapped strings, so the translator can distinguish them
    from char lists and target CakeML strings.

- basicComputeLib.sml
    Build a basic compset for evaluation in the logic.

- miscScript.sml, preamble.sml
    Theorems and proof tools (e.g. tactics) used throughout the development.

- lem_lib_stub
    empty versions of the Lem libraries (which we don't use, but building with
    Lem requires)
- lib.lem
    Extensions to Lem's built-in library to target things we need in HOL

- developers
    scripts for running regression tests and other miscellany

- COPYING
    Copyright notice, license, and disclaimer.