Hi, I'm Josh.
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.