PureCake: A Verified Compiler for a Lazy Functional Language - PLDI 2023

PureCake: A Verified Compiler for a Lazy Functional Language - PLDI 2023

Explore a 17-minute conference talk from PLDI 2023 presenting PureCake, a mechanically-verified compiler for PureLang, a lazy, purely functional programming language with monadic effects. Delve into the development of the first end-to-end correctness proof for compiling a lazy language to machine code. Learn about PureLang's Haskell-like syntax, constraint-based Hindley-Milner type system, and the derivation of sound equational reasoning principles. Discover the multiple optimization passes implemented to handle realistic lazy idioms effectively. Gain insights into the compiler's verification process, conducted entirely within the HOL4 interactive theorem prover, and its integration with the CakeML verified compiler.