Display photo

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 am now working on:

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