# AVerified 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.