Exporting CakeML to Isabelle with Lem
CakeML is a functional programming language with a proven-correct compiler and runtime system.
This repository contains an unofficial version of the CakeML semantics that has been exported from the Lem specifications to Isabelle.
The thy/generated/CakeML folder roughly corresponds to the semantics folder in the CakeML repository.
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.
Most of the files in this repository are generated automatically by the bootstrap script.
It reads configuration from the versions file that specifies which repository versions of Lem and CakeML to fetch.
After the specification has been exported, it builds the theories with isabelle build.
The thy folder corresponds to the contents of the AFP entry.
Both are kept in sync manually.
The export script and hand-written source files have been written by Lars Hupel.
Lem is a project by Peter Sewell et.al. Contributors can be found on its project page and on GitHub.
CakeML is a project with many developers and contributors that can be found on its project page and on GitHub.
In particular, Fabian Immler and Johannes Åman Pohjola have contributed Isabelle mappings for constants in the Lem specification of the CakeML semantics.