A Verified Compiler from Isabelle/HOL to CakeML

Lars Hupel, Tobias Nipkow

Many theorem provers can generate functional programs from definitions or proofs. However, this code generation needs to be trusted. Except for the HOL4 system, which has a proof producing code generator for a subset of ML. We go one step further and provide a verified compiler from Isabelle/HOL to CakeML. More precisely we combine a simple proof producing translation of recursion equations in Isabelle/HOL into a deeply embedded term language with a fully verified compilation chain to the target language CakeML.

Open access DOI
Author pdf

BibTeX:

@inproceedings{HupelN-ESOP18,
  author = {Lars Hupel and Tobias Nipkow},
  title = {A Verified Compiler from Isabelle/HOL to CakeML},
  booktitle = {European Symposium on Programming (ESOP 2018)},
  editor = {A. Ahmed},
  series = {LNCS},
  publisher = {Springer},
  volume = 10801,
  pages = "999-1026",
  year = 2018
}