CakeML_Codegen (Q51730)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry CakeML_Codegen
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | CakeML_Codegen |
AFP entry CakeML_Codegen |
Statements
Lars Hupel
0 references
This entry contains the formalization that accompanies my PhD thesis (see https://lars.hupel.info/research/codegen/). I develop a verified compilation toolchain from executable specifications in Isabelle/HOL to CakeML abstract syntax trees. This improves over the state-of-the-art in Isabelle by providing a trustworthy procedure for code generation.
0 references
8 July 2019
0 references
A Verified Code Generator from Isabelle/HOL to CakeML (English)
0 references
