Skip to content
Switch branches/tags
Go to file
Cannot retrieve contributors at this time
24 lines (19 sloc) 1003 Bytes
The CakeML project:
CakeML is a verified implementation of a significant subset of
Standard ML.
The source and proofs for CakeML are developed in the [HOL4 theorem
prover]( We use the latest development
version of [HOL4](, which we
build on [PolyML 5.7.1](
Example build instructions can be found in
Building all of CakeML (including the bootstrapped compiler and its proofs)
requires significant resources. [Built copies]( of
the compiler and resource usage for our
[regression tests]( are online.
The [master](../../tree/master) branch contains the latest development
version of CakeML. See the [version2](../../tree/version2) or
[version1](../../tree/version1) branch for previous versions.
Directory structure