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.

This YouTube video gives a nice introduction to the ideas around many of my research interests.

Currently I build support for dependent type theory and softly-typed set theory in the Isabelle proof assistant. I've also worked in machine learning and natural language processing applied to social media analysis and disaster management.

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.