Monadic Compiler Calculation (Functional Pearl)
summary
Derives a correct compiler from a correctness specification by calculating definitions during the proof, using the partiality monad to make divergence explicit and strong bisimilarity so equational reasoning stays valid; builds a small virtual machine, its exec semantics and a continuation-passing compiler, and proves correctness coinductively; handles integers, addition and a looping construct, formalized in Agda, and the method scales to several lambda calculi and effectful extensions.
AI-written summary · about
chapters (7)
- 0:00Approach overview
- 1:56Modeling diverging behavior
- 4:17Compiler specification
- 7:21Deriving integer compilation
- 10:40Handling addition logic
- 11:56Loop case and completion
- 13:33Extensions and future work
related talks
46mThe Calculated Typer (Functional Pearl)
30mCalculating Compilers for Concurrency
17mDenotation-based Compositional Compiler Verification
01h 06mVerifying a compiler through equational means
01h 01mA partial history of partial evaluation
31mPyrosome: A Framework for Modular, Extensible, Equivalence-Preserving Compilati...
09mCompilers for nothing, executables for free!- 01h 06mVerifying a compiler through equational means