We present PureCake, a mechanically-verified compiler for PureLang, a lazy, purely functional programming language with monadic effects. PureLang syntax is Haskell-like and indentation-sensitive, and its constraint-based Hindley-Milner type system guarantees safe execution. We derive sound equational reasoning principles over its operational semantics, dramatically simplifying some proofs. We prove end-to-end correctness for the compilation of PureLang down to machine code---the first such result for any lazy language---by targeting CakeML and composing with its verified compiler. Multiple optimisation passes are necessary to handle realistic lazy idioms effectively. We develop PureCake entirely within the HOL4 interactive theorem prover.

@article{paperbot1950,
  title = {PureCake: A Verified Compiler for a Lazy Functional Language},
  author = {Hrutvik Kanabar and Samuel Vivien and Oskar Abrahamsson and Magnus O. Myreen and Michael Norrish and Johannes Åman Pohjola and Riccardo Zanetti},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {7},
  number = {PLDI},
  year = {2023},
  doi = {10.1145/3591259}
}