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.
CITATION STYLE
Hupel, L., & Nipkow, T. (2018). A verified compiler from isabelle/HOL to CakeML. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10801 LNCS, pp. 999–1026). Springer Verlag. https://doi.org/10.1007/978-3-319-89884-1_35
Mendeley helps you to discover research relevant for your work.