MimIR: An Extensible and Type-Safe Intermediate Representation for the DSL Age
summary
MimIR is an extensible, higher-order IR whose core is a pure type system based on the calculus of constructions and that lets developers add domain ops as plugins called axioms with polymorphic, polytypic, or dependent types. It implements smart constructors, normalization rules, and a filter-driven partial evaluation to keep typechecking decidable, proves progress/preservation for the core calculus, and compiles three case studies (LLVM-style low-level, regex, tensor+AD) with state-of-the-art performance and available artifacts.
AI-written summary · about
chapters (11)
- 0:00MimIR and DSLs intro
- 2:55MLIR limitations for DSLs
- 4:18MimIR design and type system
- 6:26Defining plugins and ops
- 8:09MimIR type system and dependent types
- 10:21Normalization and type checking
- 12:32Recursion and partial evaluation
- 14:22Control flow with continuations
- 15:25Specializations and loop unrolling
- 16:07MimIR expressiveness and performance
- 17:13Q&A
related talks
18mGraph IRs for Impure Higher-Order Languages: Making Aggressive Optimizations Af...
25mNice to Meet You: Synthesizing Practical MLIR Abstract Transformers
01h 05mSemantic Intermediate Representations for Sound Language Interoperability
27mR Melts Brains -- An IR for First-Class Environments and Lazy Effectful Arguments
48mCross-Domain Compilation: Exploiting Synergies Across the CS Community
30mAnalyzing Programs with SMT Solvers
33mTeIL: a type-safe imperative Tensor Intermediate Language
01h 05mAll the Languages Together