Skip to content
This repository

CakeML: A Verified Implementation of ML

minor moving of some lemmas around

mainly into miscTheory
latest commit c3fd5a3c2f
Ramana Kumar authored
Octocat-spinner-32 bootstrap finish the equality types cheats February 21, 2014
Octocat-spinner-32 bytecode can_Print made stricter, compiler proofs updated February 24, 2014
Octocat-spinner-32 compiler add a couple defs to bytecode_emitScript.sml March 12, 2014
Octocat-spinner-32 developers translate new HOL implementation into CakeML March 19, 2014
Octocat-spinner-32 hol-light minor moving of some lemmas around March 20, 2014
Octocat-spinner-32 inference rename String constructor to StrLit February 05, 2014
Octocat-spinner-32 lem_lib_stub compilation of string literals February 05, 2014
Octocat-spinner-32 metatheory rename String constructor to StrLit February 05, 2014
Octocat-spinner-32 new-backend minor tweak February 21, 2014
Octocat-spinner-32 parsing update parser to handle string literals February 01, 2014
Octocat-spinner-32 repl major update of x64_heap February 18, 2014
Octocat-spinner-32 sem-reason More sketching on the logical relation August 19, 2013
Octocat-spinner-32 semantics rename a List_extra function in lib.lem March 11, 2014
Octocat-spinner-32 translator only translate 8-bit words March 19, 2014
Octocat-spinner-32 unverified Update README August 16, 2013
Octocat-spinner-32 whole-prog update wholeProgScript.sml for changes to bytecode February 06, 2014
Octocat-spinner-32 x86-64 some progress on x86-64 proofs March 20, 2014
Octocat-spinner-32 .gitignore Write a basic shell-script to do some regression testing. July 29, 2013
Octocat-spinner-32 COPYING add copyright notice, license, and disclaimer July 25, 2013
Octocat-spinner-32 README remove clockScript.sml from README January 15, 2014
Octocat-spinner-32 miscLib.sml Reorganise hol-light into subdirectories. January 11, 2014
Octocat-spinner-32 miscScript.sml minor moving of some lemmas around March 20, 2014
Octocat-spinner-32 preamble.sml Initial commit October 09, 2012
The CakeML project. See and

A verified implementation of a significant subset of Standard ML in the HOL4
theorem prover (

NB: We develop this using the head of the HOL4 development version in Github
(, and it will not work on official HOL releases.
We build HOL on PolyML 5.5 ( Also, a full build
(including the bootstrapping which runs the compiler on itself in the logic)
may require 16GB RAM.

Directory structure:

- semantics
    The definition of CakeML, including
    - its concrete syntax
    - its abstract syntax
    - small step semantics
    - big step semantics
    - a type system
    The definition is (mostly) expressed in
    Lem (,
    but the generated HOL is also included.

- metatheory
    Proofs about CakeML, including
    - type soundness
    - determinism
    - equivalence of the big and small step semantics
    - a verified clocked interpreter

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

- repl
    The REPL implementation in HOL.
    Defines repl_fun : string -> repl_result.
    Also includes some machinery for evaluating repl_fun in the logic.
- repl/proofs
    The correctness proof for repl_fun.
- repl/examples
    Examples of evaluating repl_fun in the logic.

- whole-prog
    Compile a whole CakeML program to 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.
- translator/repl/proofs
    Theorem about the correctness of the result of bootstrapping the above, as
    done below.

- bootstrap
    Evaluation of the compiler on the deep embedding of repl_fun produced by
    the translator.

- x86-64
    (Work towards an) x86-64 implementation of repl_fun.

- 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 (
    in CakeML.

    Copyright notice, license, and disclaimer.
Something went wrong with that request. Please try again.