Verified Compilation and Optimization of Floating-Point Programs in CakeML
No abstract available.
Related papers
- Icing: Supporting Fast-Math Style Optimizations in a Verified Compiler CAV 2019
- The pitfalls of verifying floating-point computations TOPLAS 2008
- A Verified Compiler from Isabelle/HOL to CakeML ESOP 2018
- Brack: A Verified Compiler for Scheme via CakeML CPP 2026
- Verifying bit-manipulations of floating-point PLDI 2016
- A new verified compiler backend for CakeML ICFP 2016
- CakeML: a verified implementation of ML POPL 2014
- Verified compilation of CakeML to multiple machine-code targets CPP 2017