PureCake

A verified compiler for a lazy functional language

PureCake is a verified implementation of a small, Haskell-like language known as PureLang. It targets CakeML, a verified implementation of a significant subset of Standard ML. PureCake is developed within the HOL4 interactive theorem prover.

Quick start

docker run -it ghcr.io/cakeml/pure:master

This Docker image contains a pre-built version of the PureCake compiler.

Quick start without Docker

git clone https://github.com/cakeml/pure
cd pure/examples && make download

This downloads the latest pre-built version of the PureCake compiler from GitHub. You can now compile PureLang programs without building the compiler yourself, as described in examples/README.md.

Slow start

Follow the build process described by our Dockerfile. In summary: install PolyML; build HOL4; clone the PureCake and CakeML repositories; run Holmake in the top-level of the PureCake repository. Building the entire PureCake project (including the bootstrapped compiler) will take several hours and require considerable compute resources.

Repository structure

COPYING: PureCake Copyright Notice, License, and Disclaimer.

compiler: A verified compiler from PureLang to CakeML, with the components below.

• backend: the compiler backend, with the following subdirectories.
  • languages: intermediate languages, their semantics, and derived properties.
  • passes: compilation passes and their proofs of correctness.
• binary: verified (in-logic) bootstrapping of a compiler binary.
• parsing: lexing and parsing expression grammar (PEG) parsing.
• proofs overall proofs of correctness.
• pure_compilerScript.sml: the compiler's top-level definition.

examples: Examples of PureLang code, how to invoke the PureCake compiler on them, and how to measure their performance.

language: Definitions concerning PureLang and its semantics, including built-in operations.

meta-theory: PureLang's meta-theory. In particular, PureLang's equational theory and associated proofs (e.g. soundness of alpha- and beta-equivalence, and coincidence with contextual equivalence), and a formalisation of strictness (demands).

misc: Miscellaneous lemmas.

typing: PureCake's type system: proof of type soundness and a verified type inferencer.