A Verified Compiler from Isabelle/HOL to CakeML
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
}