Email Gateway (Aug 22 2022 at 16:58): Email Gateway (Aug 22 2022 at 16:58):From: Gerwin.Klein@data61.csiro.au
Usually, we avoid adding new entries to the development version of the AFP, but this one is an exception:
CakeML
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.
The project has many contributors:
The export script and hand-written source files are by Lars Hupel. Lem is a project by Peter Sewell et. al. CakeML is a project with many developers and contributors that can be found on its project page [https://cakeml.org] 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.
The entry is now available from the repository at https://bitbucket.org/isa-afp/afp-devel and it will become available from https://isa-afp.org with the next Isabelle release.
Enjoy!
Gerwin
Last updated: Nov 21 2024 at 12:39 UTC