The author possesses high engineering skill in compiler technology, and decent engineering skill in formalization with Coq.
- An introduction to auto-vectorization with LLVM
- Deficiencies in LLVM's LoopVectorize
- Incrementally updating the Dominator
- Detecting loops
- Inside a register allocator
- An ABI-mismatch bug
- Predicativity in Coq
- Equality in Mechanized Mathematics
- Lean versus Coq: The cultural chasm