About

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:

Getting started

The latest version of PureCake can be found in our Docker image below. Please refer to the README.md.

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

More information

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 Zenodo. The README.md explains how to replicate all of our results.

docker run -it ghcr.io/cakeml/pure-pldi-artifact

Getting involved

If you are interested in contributing to PureCake or have any questions, please visit our GitHub repository and join our Discord (with this link) and see the #pure channel.

Compiler structure

The current version of PureCake uses 3 intermediate languages.