Tobias Grosser¶
Associate Professor
University of Cambridge
I lead the Cambridge Compiler Lab, where we work on compilation, programming language design, and performance programming. We combine strong mathematical foundations with production-quality engineering, and build our tools in the open, together with the LLVM, MLIR, and Lean communities. I define these areas broadly and ask questions such as:
- Can we prove compilers correct, and make formal verification part of everyday compiler engineering?
- Can compilers revolutionize how hardware, from ASICs to CPUs, is designed?
- How can AI help us automate compiler design, and how can compilers make AI faster?
- How can compilers help scientists understand climate change?
- How can performance programming become a smooth and interactive experience for developers?
Before joining Cambridge, I was a Reader at the University of Edinburgh, an Ambizione Fellow at ETH Zurich, and a Google PhD Fellow at École Normale Supérieure Paris. I studied computer science as an undergraduate at the University of Passau in Germany.
Latest papers¶
- OOPSLA 2026Sound and Complete Solving for Multi-width Parametric Bitvectors via Principled Reductions
- ICS 2026An Open-Source-First Approach: Multi-Level Compiler Design for AI and HPC
- ASPLOS 2026An MLIR Lowering Pipeline for Stencils at Wafer-Scale
- ASPLOS 2026The Configuration Wall: Characterization and Elimination of Accelerator Configuration Overhead
- OOPSLA 2025Certified Decision Procedures for Width-Independent Bitvector Predicates
Latest talks¶
Scaling Certified Instruction Selection For LLVM IR Through Bitblasting
Sarah Linh Kuhn, Luisa Cicolini
An LLVM instruction selector verified in Lean: using Sail's Lean backend for authoritative RISC-V semantics, we automatically verify real LLVM instruction selection and optimization patterns.
Toward A More Declarative InstCombine: Generalization & Parametric Bitvector Algorithms
New parametric bitvector algorithms lift InstCombine's fixed-width tests into width-independent identities, moving LLVM toward a declarative, provably correct InstCombine.
Specializing MLIR Data Structures: an Experiment
What happens when we specialize MLIR's core data structures for a single dialect? Challenges, solutions, and lessons for faster MLIR compilers.