A Verified Code Generator from Isabelle/HOL to CakeML

Title:	A Verified Code Generator from Isabelle/HOL to CakeML
Author:	Lars Hupel
Submission date:	2019-07-08
Abstract:	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.
BibTeX:	@article{CakeML_Codegen-AFP, author = {Lars Hupel}, title = {A Verified Code Generator from Isabelle/HOL to CakeML}, journal = {Archive of Formal Proofs}, month = jul, year = 2019, note = {\url{https://isa-afp.org/entries/CakeML_Codegen.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Depends on:	CakeML, Constructor_Funs, Dict_Construction, Higher_Order_Terms, Huffman, Pairing_Heap, Root_Balanced_Tree, Show
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.