We present some recent work on homotopy type theory, while cubical type theory work is in preparation. Earlier work investigates compiler technology; middle-end loop optimizations in particular.
-
Is there a type theory for
𝕠 𝕡 - Sets and Logic
- The essentials
- The type theory
- Incrementally updating the Dominator
- Detecting loops
- Inside a register allocator
- An ABI-mismatch bug