CakeML

Lars Hupel and Yu Zhang with contributions from Johannes Åman Pohjola

12 March 2018

Abstract

CakeML is a functional programming language with a proven-correct compiler and runtime system. This entry contains an unofficial version of the CakeML semantics that has been exported from the Lem specifications to Isabelle. Additionally, there are some hand-written theory files that adapt the exported code to Isabelle and port proofs from the HOL4 formalization, e.g. termination and equivalence proofs.
BSD License

Depends On

Used by

Topics

Theories

Cite

×
@article{CakeML-AFP,
  author  = {Lars Hupel and Yu Zhang},
  title   = {CakeML},
  journal = {Archive of Formal Proofs},
  month   = March,
  year    = 2018,
  note    = {\url{http://isa-afp.org/entries/CakeML.html},
            Formal proof development},
  ISSN    = {2150-914x},
}
Download