MimIR: An Extensible and Type-Safe Intermediate Representation for the DSL Age
This program is tentative and subject to change.
Traditional compilers, designed for optimizing low-level code, fall short when dealing with modern, computation-heavy applications like image processing, machine learning, or numerical simulations. Optimizations should understand the primitive operations of the specific application domain and thus happen on that level.
Domain-specific languages (DSLs) fulfill these requirements. However, DSL compilers reinvent the wheel over and over again as standard optimizations, code generators, and general infrastructure & boilerplate code must be reimplemented for each DSL compiler.
This paper presents MimIR, an extensible, higher-order intermediate representation. At its core, MimIR is a pure type system and, hence, a form of a typed lambda calculus. Developers can declare the signatures of new (domain-specific) operations, called “axioms”. An axiom can be the declaration of a function, a type operator, or any other entity with a possibly polymorphic, polytypic, and/or dependent type. This way, developers can extend MimIR at any low or high level and bundle them in a plugin. Plugins extend the compiler and take care of optimizing and lowering the plugins’ axioms.
We show the expressiveness and effectiveness of MimIR in three case studies: Low-level plugins that operate at the same level of abstraction as LLVM, a regular-expression matching plugin, and plugins for linear algebra and automatic differentiation. We show that in all three studies, MimIR produces code that has state-of-the-art performance.
This program is tentative and subject to change.
Fri 24 JanDisplayed time zone: Mountain Time (US & Canada) change
10:40 - 12:00 | |||
10:40 20mTalk | MimIR: An Extensible and Type-Safe Intermediate Representation for the DSL Age POPL Roland Leißa University of Mannheim, School of Business Informatics and Mathematics, Marcel Ullrich Saarland University, Joachim Meyer Compiler Design Lab; Saarland Informatics Campus; Saarland University, Sebastian Hack Saarland University, Saarland Informatics Campus | ||
11:00 20mTalk | Simple Linear Loops: Algebraic Invariants and Applications POPL Rida Ait El Manssour CNRS & IRIF, Paris, George Kenison Liverpool John Moores University, Mahsa Shirmohammadi CNRS & IRIF, Paris, Anton Varonka TU Wien | ||
11:20 20mTalk | Automated Program Refinement: Guide and Verify Code Large Language Model with Refinement Calculus POPL Yufan Cai National University of Singapore, Zhe Hou Griffith University, David Sanan Nanyang Technological University, Singapore, Xiaokun Luan Peking University, Yun Lin Shanghai Jiao Tong University, Jun Sun Singapore Management University, Jin Song Dong National University of Singapore | ||
11:40 20mTalk | Tail Modulo Cons, OCaml, and Relational Separation Logic POPL Clément Allain INRIA, Frédéric Bour Tarides, Basile Clément OCamlPro, François Pottier Inria, Gabriel Scherer Université Paris Cité - Inria - CNRS |