A Verified Code Generator from Isabelle/HOL to CakeML

Lars Hupel 🌐

July 8, 2019

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


This entry contains the formalization that accompanies my PhD thesis (see https://lars.hupel.info/research/codegen/). I develop a verified compilation toolchain from executable specifications in Isabelle/HOL to CakeML abstract syntax trees. This improves over the state-of-the-art in Isabelle by providing a trustworthy procedure for code generation.


BSD License


Session CakeML_Codegen