Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
CakeML: A Verified Implementation of ML
Standard ML Other
Failed to load latest commit information.
bootstrap translate anub (required MEMBER_INTRO for the induction thm)
bytecode start strengthening definition of code_executes_ok
compiler add handler=0 condition to env_rs
developers add targets/arm8 to build-sequence
documentation More manual writing
explorer explorer no longer depends on x86-64/
hol-light improve case exps in rev_assocd and codomain
inference move anub and lemmas into miscTheory
initial Merge remote-tracking branch 'origin/master' into infcomp3
lem_lib_stub tweaks to make lem files build with latest lem
metatheory a bit of progress on one of the completeness cheats
new-backend Removed cheat in the allocator translation
parsing Bunch of changes in light of HOL's change to Q's match/rename tactics.
repl Merge remote-tracking branch 'origin/master' into infcomp3
sem-reason More sketching on the logical relation
semantics Merge remote-tracking branch 'origin/master' into infcomp3
standalone standalone no longer depends on x86-64/
targets Modify ASM so that CakeML can target big-endian architectures.
translator improve case exps in rev_assocd and codomain
unverified comment out more code_labels_ok stuff
x86-64 Merge remote-tracking branch 'origin/master' into infcomp3
.gitignore gitignore x86-64 test dirs
.travis.yml add sudo: false to travis, to take advantage of docker
COPYING update copyright holders and years
Holmakefile Start on refactoring the CakeML compset infrastructure
README Update HOL URL in README.
compute_basicLib.sml Start on refactoring the CakeML compset infrastructure
miscLib.sml fix bug in join_EVERY
miscScript.sml move anub and lemmas into miscTheory
mlstringLib.sig conversion for translating literal mlstring case splits to if-then-else
mlstringLib.sml make mlstring_case_conv slightly more robust/lenient
mlstringScript.sml define mlstring_cmp from mlstring_lt
mlstringSyntax.sig add strlit syntax fns to mlstringSyntax
mlstringSyntax.sml add mlstring_case syntax fns
preamble.sml Add a HOL heap to bytecode

README

The CakeML project. See https://cakeml.org and https://github.com/CakeML.

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

NB: We develop this using the head of the HOL4 development version in Github
(https://github.com/HOL-Theorem-Prover/HOL), and it will not work on official HOL releases.
We build HOL on PolyML 5.5.2 (http://www.polyml.org/). Also, a full build
(including the bootstrapping which runs the compiler on itself in 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
    Definition of the initial program that sets up the initial
    environment for CakeML programs.

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

- new-backend
- targets
    Work towards a new series of compilation phases to replace the bytecode.

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

- sem-reason
    Work towards logical tools for reasoning about CakeML programs.

- 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.
Something went wrong with that request. Please try again.