Skip to content

Research

We build compilers that combine strong mathematical foundations with production-quality engineering. Our work is open source and developed together with the LLVM, MLIR, and Lean communities, so that our results reach the compilers people use every day. Five themes run through our research.

Verified compilation

Compilers are trusted to get every rewrite right, yet they are among the most complex software we have. We make formal verification part of everyday compiler engineering: in the Lean proof assistant we build decision procedures for bitvectors, verify peephole rewrites from LLVM and MLIR, and certify instruction selection against official ISA semantics.

Project: Lean-MLIR: Verified Compilation in Lean
Key papers:

Compiler infrastructure

Building a compiler should not require years of expertise. We design the abstractions that make compilers modular and easy to build: declarative IR definitions, Python-native compiler prototyping with xDSL, and e-graphs as a first-class compiler abstraction. Much of this work is part of MLIR upstream.

Project: High-Productivity Compiler Development
Key papers:

Hardware design and accelerators

Compilers can change how hardware is designed and how accelerators are used. We build multi-level IRs for hardware description, compile for RISC-V extensions and custom accelerators, and remove the configuration overhead that holds accelerators back.

Projects: Open-Source Electronic Design Automation, Seamless Design of Smart Edge Processors
Key papers:

Compilers for AI, science, and quantum computing

Domain-specific compilers turn high-level programs into fast code for specialised hardware. We compile stencil codes from climate and physics simulations down to wafer-scale engines, generate efficient code for structured tensor algebra, and design IRs for hybrid quantum-classical programs.

Project: Compilation for Quantum Computers
Key papers:

Performance programming

Fast code needs precise models of programs and hardware. We develop fast Presburger arithmetic for polyhedral analysis, analytical cache models, and techniques to find missed optimizations, with the goal of making performance programming an interactive play between programmer and compiler.

Project: FPL: A Fast Presburger Library
Key papers:

Learn more

In The Compilation Game, I describe our vision of compilation as an interactive game between programmers and compilers:

See all our publications, projects, and talks, or join us.