Computing

The author possesses high engineering skill in compiler technology (C++), and decent engineering skill in formalization with a proof assisant (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