[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!

Larry Paulson

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.