A Verified Code Generator from Isabelle/HOL to CakeML

Lars Hupel 🌐

July 8, 2019

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

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.

License

BSD License

Topics

Session CakeML_Codegen

Depends on

Cite

× 
@article{CakeML_Codegen-AFP,
  author  = {Lars Hupel},
  title   = {A Verified Code Generator from Isabelle/HOL to CakeML},
  journal = {Archive of Formal Proofs},
  month   = {July},
  year    = {2019},
  note    = {\url{https://isa-afp.org/entries/CakeML_Codegen.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: