Early works investigates compilers, and later work investigates homotopy type theory
- Is there a type theory for $\mathbb{Top}_*$?
- Sets and Logic
- The essentials
- The type theory
- Incrementally updating the Dominator
- Detecting loops
- Inside a register allocator
- An ABI-mismatch bug