Calculating Compilers for Concurrency
summary
Paper shows a method that turns a high‑level choice trees semantics into a correct-by-construction compiler by adding a codensity construction, yielding algebraic laws that let calculation produce both target code and its semantics. Results include a derived stack-machine with new instructions (Push, Fork) and a compiler for a higher‑order concurrent lambda calculus with channel communication, formalized and checked (DOI:10.1145/3607855) with a reusable artifact archive (DOI:10.5281/zenodo.8124116).
AI-written summary · about
chapters (12)
- 0:00Introduction
- 0:44Calculating a compiler
- 3:12Concurrent language monad
- 5:40Choice trees semantics
- 8:10Flaws in fork semantics
- 12:27Codensity monads fix
- 15:42Compiler for concurrency
- 18:31Compiler for literals
- 22:22Compiler for fork
- 24:11Summary
- 24:31Paper details
- 25:36Q&A
related talks
15mMonadic Compiler Calculation (Functional Pearl)
23mCorrect Compilation of Concurrent C Code
30mMonadic interpreters for concurrent memory models: Executable semantics of a concurrent(…)
25mA Lazy, Concurrent Convertibility Checker
31mPyrosome: A Framework for Modular, Extensible, Equivalence-Preserving Compilati...
01h 01mThe Future of Concurrency and Parallelism
13mCompiling Classical Sequent Calculus to Stock Hardware: The Duality of Compilation
01h 05mControl Flow Obfuscation for Featherweight Java + Efficient Fair Conjunction