Email Gateway (Aug 22 2022 at 20:14): Email Gateway (Aug 22 2022 at 20:14):From: Lawrence Paulson <lp15@cam.ac.uk>
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
Last updated: Apr 26 2024 at 16:20 UTC