The author possesses high engineering skill in compiler technology, and decent engineering skill in formalization with Coq. coq (2020) Predicativity in Coq Equality in Mechanized Mathematics Lean versus Coq: The cultural chasm compilers (2015 — 2016) Incrementally updating the Dominator Detecting loops Inside a register allocator An ABI-mismatch bug