Display photo

Hi, I'm Josh.

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


My current work is in formal verification and interactive theorem proving. In particular, my goal is to make 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.

More technically, I build logics and tools for the Isabelle and Coq proof assistants. At the moment I'm 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

PDF here.