A verified compiler for a lazy functional language
PureCake is a HOL4-verified compiler for PureLang: a Haskell-inspired, lazy, purely functional programming language with monadic effects. PureCake correctly compiles PureLang to CakeML source, composing with its verified compiler to produce end-to-end guarantees. Aside from verified compilation, PureCake provides:
- Haskell-like, indentation-senstive syntax
- Sound equational reasoning
- Two-phase, constraint-based Hindley-Milner type inference
- Verified demand analysis
- Verified optimisations for handling realistic lazy idioms (e.g. monadic reflection)
The talk below gives an overview of the PureCake development:
The latest version of PureCake can be found in our Docker image below.
Please refer to the
docker run -it ghcr.io/cakeml/pure:master
The ideas behind the PureCake development are described in our PLDI'23 paper:
PureCake: A Verified Compiler for a Lazy Functional Language.
The version described in this paper can be found in the Docker image below or on
README.md explains how to replicate all of our results.
docker run -it ghcr.io/cakeml/pure-pldi-artifact