CakeML

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

March 12, 2018

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

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

Topics

Theories of LEM

Theories of CakeML