This repository has been archived by the owner on Aug 8, 2020. It is now read-only.
Releases: larsrh/isabelle-cakeml
Releases · larsrh/isabelle-cakeml
Isabelle/CakeML v1.0
v1.0
This tag was signed with the committer’s verified signature.
The key has expired.
larsrh
Lars Hupel
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.
Based on v2.0 of CakeML.
This is the version that has been initially submitted to the Archive of Formal Proofs.