Display photo

Hi, I'm Josh.

I'm a Ph.D. student researcher working on the SMART project at the Computational Logic group of the University of Innsbruck.

Find me online elsewhere:


I'm interested in the development of better logical foundations and interactive proof assistants for mathematics, with a particular bent towards homotopy type theory and univalent foundations.

Currently I build support for dependent type theory and softly-typed set theory in the Isabelle proof assistant.

Previously, I studied mathematics at the University of Bonn and the Australian National University. For my masters thesis I implemented a homotopy type theory object logic for Isabelle, while my bachelors thesis was on quantum algebra, TQFTs, and an application to invariants of topological manifolds.