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.
Overview
Syllabus
Introduction
Language guarantees
Binary level guarantees
Verified compilation
PureCake
PureLang
PureLang features
Compiler Expressions
Operational Semantics
Compiler
Type Inference
Demand Analysis
Compiler Backend
Syntax Relations
ThunLang
StateLang
Endtoend correctness
Questions
Taught by
ACM SIGPLAN
