The CakeML project. See https://cakeml.org.

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

This branch, version1, is a release branch. Continued development happens on master.

This release works with:
  HOL4 version 0106cc6 or later. (TODO: replace once there is another HOL release)
  PolyML 5.5.2 (http://www.polyml.org)

To build the verified REPL:
  cd x86-64/wrapper
  Holmake cake

A full build, which includes bootstrapping the compiler within the logic, may
require 8GB RAM.

Directory structure:

- semantics
    The definition of CakeML, including
    - its concrete syntax
    - its abstract syntax
    - small step semantics
    - big step semantics
    - a type system
    - a verified, clocked interpreter (in the proofs/ sub-directory)
    - basic facts about the semantics (including determinism) in the proofs/
      sub-directory
    The definition is (mostly) expressed in
    Lem (http://www.cs.kent.ac.uk/~sao/lem),
    but the generated HOL is also included.

- metatheory
    Proofs about CakeML, including
    - type soundness
    - equivalence of the big and small step semantics

- parsing
    Lexer and PEG parser for CakeML.

- inference
    Type inferencer for CakeML.
- inference/proofs
    Proof of soundness for the type inferencer.

- bytecode
    CakeML Bytecode specification, metatheory, and evaluator.

- compiler
    Compiler from CakeML abstract syntax to CakeML Bytecode, with the
    implementation expressed in Lem.
- compiler/proofs
    Verification of the compiler.

- initial
    Proofs about the initial program and the initial
    environment for CakeML programs that it sets up.

- repl
    The REPL implementation in HOL.
    Defines repl_fun : string -> repl_result.
- repl/proofs
    The correctness proof for repl_fun.

- standalone
    Compile a whole CakeML program to x86 (or bytecode), instead of
    interleaving compilation and execution as in the REPL.

- translator
    A proof-producing translator from HOL functions to CakeML.
- translator/repl
    A run of the translator on the translatable part of repl_fun.

- bootstrap
    Evaluation of the compiler on the deep embedding of repl_fun produced by
    the translator, and proofs about the result.

- x86-64
    x86-64 implementation of repl_fun and the runtime.

- unverified/interp
    Unverified implementation, in Haskell, of the CakeML frontend augmented
    with informative error messages.
- unverified/bytecode
    An unverified implementation of CakeML bytecode, written in C

- hol-light
    An implementation of HOL Light (http://www.cl.cam.ac.uk/~jrh13/hol-light/)
    in CakeML.

- 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.

- compute_basicLib.sml
    Build compsets for evaluation in the logic.

- miscLib.sml, 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)

- developers
    scripts for running regression tests and other miscellany

- COPYING
    Copyright notice, license, and disclaimer.