[isabelle] New in the AFP: A Verified Code Generator from Isabelle/HOL to CakeML
I’m happy to announce this substantial new contribution:
> 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.
This looks to be a major importance and I hope we will get some instructions on how to use it!
This archive was generated by a fusion of
Pipermail (Mailman edition) and