I am a research software engineer at Microsoft Research in the RiSE group.

I have been the main developer of GAPT since 2015; GAPT is a library for classical proof theory developed at TU Wien supporting reliable proof import from almost a dozen external theorem provers.

I have developed the current parallel compilation infrastructure and interactive editor integration for the Lean theorem prover. I have designed the homotopy type theory support for Lean 3. I have also written an independent reference type checker for Lean, trepplein.