Hi, I'm Josh!

I'm a first-year Ph.D. student in the SMART project at the Computational Logic group of the University of Innsbruck.

My current research focuses on making interactive proof assistants more powerful and at the same time simpler to use, in order to become daily tools for mathematicians and computer scientists alike.


I'm currently working on softly-typed set-theoretic foundations in Isabelle, as well as proof automation and hammer systems for Coq.

I'm also interested in type theory (homotopy and otherwise), univalent foundations, and mathematical logic.

Previously, I studied mathematics at the University of Bonn and the Australian National University. For my masters thesis with Peter Koepke I implemented a version of homotopy type theory as an Isabelle object logic. My bachelors thesis under Scott Morrison was on quantum algebra, TQFTs, and an application to diagrammatic invariants of topological manifolds.



Curriculum vitae