@InProceedings{10.1007/978-3-319-89884-1_35,
author="Hupel, Lars
and Nipkow, Tobias",
editor="Ahmed, Amal",
title="A Verified Compiler from Isabelle/HOL to CakeML",
booktitle="Programming Languages and Systems",
year="2018",
publisher="Springer International Publishing",
address="Cham",
pages="999--1026",
abstract="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.",
isbn="978-3-319-89884-1"
}