Explore the metatheory of Intermediate Representations (IRs) and the CPS-calculus in this 12-minute conference talk from POPL'23. Delve into the relationship between programming languages and calculi, focusing on the limitations of the λ-calculus for certain situations. Examine the CPS-calculus as a representative for IRs, its equational theory based on compiler optimizations, and its metatheoretical properties. Learn about the calculus' strong normalization in a simply-typed setting and its potential as a logic system. Discover how this research contributes to proving optimizations sound and opens new paths for safe compilation of dependently-typed programming languages.
Overview
Syllabus
Introduction
A crash course into the CPS-calculus - semantics
Comparison to actual compiler IRS
Contribution: extending the semantics
Results: factorization and adequacy
Results: strong normalization
Conclusions and Future Work
Taught by
ACM SIGPLAN
