Graph IRs for Impure Higher-Order Languages: Making Aggressive Optimizations Af...
summary
A typed graph IR combines reachability types with an effect system to compute precise, flow-sensitive effect dependencies without CFA by doing type-based inference; it embeds lexical lambda nodes so the IR supports interprocedural code motion, lambda hoisting, inlining, and anti-dependence-based DCE while remaining modular for separate compilation. Implementation in Scala LMS shows case studies (tensor loop fusion, CUDA kernel fusion, symbolic LLVM execution, SQL and Datalog compilation) with validated soundness and mechanized meta-theory and speedups up to 21x.
AI-written summary · about
chapters (9)
- 0:00Graph IRs introduction
- 2:56Higher-order effectful challenges
- 4:44Reachability types for dependencies
- 7:14Graph edge dependencies
- 8:37Lexical structure in graphs
- 10:46Graph optimizations and dependencies
- 12:53Implementation and performance
- 14:41Code generation and frequency
- 15:24Q&A
related talks
20mMimIR: An Extensible and Type-Safe Intermediate Representation for the DSL Age
27mR Melts Brains -- An IR for First-Class Environments and Lazy Effectful Arguments
01h 05mSemantic Intermediate Representations for Sound Language Interoperability
48mCross-Domain Compilation: Exploiting Synergies Across the CS Community
21mVerifying term graph optimizations using Isabelle/HOL
25mNice to Meet You: Synthesizing Practical MLIR Abstract Transformers
22mReconciling High-level Optimizations and Low-level Code in LLVM
12mOn the metatheory of IRs and the CPS-calculus