CakeML

 Title: CakeML Authors: Lars Hupel and Yu Zhang Contributor: Johannes Åman Pohjola Submission date: 2018-03-12 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. BibTeX: @article{CakeML-AFP, author = {Lars Hupel and Yu Zhang}, title = {CakeML}, journal = {Archive of Formal Proofs}, month = mar, year = 2018, note = {\url{http://isa-afp.org/entries/CakeML.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License Depends on: Coinductive, IEEE_Floating_Point, Show Used by: CakeML_Codegen 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.