Fetching contributors…
Cannot retrieve contributors at this time
89 lines (71 sloc) 3 KB
The CakeML project (
A verified implementation of a significant subset of Standard ML in the HOL4
theorem prover (
We build CakeML using the latest development version of HOL4.
We build HOL on PolyML 5.6 (
Example build instructions can be found in
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 (,
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
(, 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
Copyright notice, license, and disclaimer.