CakeML is an activity of Trustworthy Systems.
AimReducing the cost and increasing the guarantees of verified software.
- Verified compilation: we have developed the world-leading verified optimising compiler (and runtime system) for functional programming.
- Proof-producing code generation: we have developed methods for automatically producing (verified) CakeML implementations of algorithms defined and verified in higher-order logic.
See the CakeML project website.
CakeML is a collaborative effort by researchers at multiple institutions. At Data61, we have:
- A New Verified Compiler Backend for CakeML, ICFP'16
- Functional Big-step Semantics, ESOP'16
- A Verified Type System for CakeML, IFL'15
- Pattern Matches in HOL: A New Representation and Improved Code Generation, ITP'15
- CakeML: A Verified Implementation of ML, POPL'14
- Proof-Producing Translation of Higher-Order Logic into Pure and Stateful ML, JFP'14
- Proof-Producing Synthesis of ML from Higher-Order Logic, ICFP'12