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 master
version of HOL4, which we
build on PolyML 5.7.1.
Example build instructions can be found in
build-instructions.sh.
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 branch contains the latest development
version of CakeML. See the version2 or
version1 branch for previous versions.
Directory structure
LICENSE:
BSD 3-Clause License
basis:
Contains the beginnings of a standard basis library for CakeML,
similar to the standard basis library of SML.
build-instructions.sh:
This file describes how to install Poly/ML, HOL and CakeML.
candle:
Verification of a HOL theorem prover, based on HOL Light
(http://www.cl.cam.ac.uk/~jrh13/hol-light/), implemented in CakeML.
characteristic:
A verified CakeML adaption of Arthur Charguéraud's "Characteristic
Formulae for the Verification of Imperative Programs"
compiler:
A verified compiler for CakeML, including:
- lexing and PEG parsing,
- type inference,
- compilation to ASM assembly language, and,
- code generation to x86, ARM, and more.
cv_translator:
Translator to the cv type used by cv_compute.
developers:
This directory contains scripts for automating routine tasks, e.g., for
generating README.md files.
examples:
Examples of verified programs built using CakeML infrastructure.
how-to.md:
This document introduces how to use the CakeML compiler, providing in
particular:
- a description of how to invoke the CakeML compiler,
- a list of how CakeML differs from SML and OCaml, and,
- a number of small CakeML code examples.
misc:
Auxiliary files providing glue between a standard HOL installation
and what we want to use for CakeML development.
pancake:
The Pancake compiler, i.e. a C-like compiler built from the lower
parts of the CakeML compiler.
profiler:
Basic profiling facilities for theories and proofs.
semantics:
The definition of the CakeML language.
The directory includes definitions of:
- the concrete syntax,
- the abstract syntax,
- big step semantics (both functional and relational),
- a small step semantics,
- the semantics of FFI calls, and,
- the type system.
translator:
A proof-producing translator from HOL functions to CakeML.
tutorial:
An extended worked example on using HOL and CakeML to write verified programs,
that was presented as a tutorial on CakeML at PLDI and ICFP in 2017.
unverified:
Various unverified tools, e.g. tools for converting OCaml to CakeML
and an SML version of the CakeML register allocator.
