On the metatheory of IRs and the CPS-calculus
summary
Formalizes Thielecke’s CPS-calculus with an equational theory driven by real compiler optimizations and proves the new reduction relation admits a theory of residuals, is confluent and factorisable, and agrees with the compiler’s leftmost-prefix execution so optimizations transfer soundly to IRs. Shows the simply-typed CPS-calculus is strongly normalizing (simply-typed), draws a Curry‑Howard link to the negative fragment of polarized linear logic, and ships as 16,000 lines of Coq on GitHub.
AI-written summary · about
chapters (7)
- 0:00Introduction
- 3:43A crash course into the CPS-calculus - semantics
- 5:31Comparison to actual compiler IRS
- 6:44Contribution: extending the semantics
- 8:22Results: factorization and adequacy
- 9:31Results: strong normalization
- 10:45Conclusions and Future Work
related talks
15mCompiling with Continuations, Correctly
31mPyrosome: A Framework for Modular, Extensible, Equivalence-Preserving Compilati...
29mHigher-Order Weakest Precondition Transformers via a CPS Transformation
13mOne-Pass CPS Translation of Dependent Types (Talk Proposal)
18mGraph IRs for Impure Higher-Order Languages: Making Aggressive Optimizations Af...
19mTowards a Reflection for Effect Handlers
29mA Typed and Unified Reflection for Shift and Shift0
19mExtensible Metatheory Mechanization via Family Polymorphism