Hi, I'm Josh.
Find me online elsewhere:
My current work is in formal verification and interactive theorem proving. I work towards 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.
More technically, I build logics and tools for the Isabelle proof assistant, currently working on support for dependent type theory and softly-typed set theory. I'm also interested in type theory (homotopy and otherwise), univalent foundations and mathematical logic.
Previously, I studied mathematics at the University of Bonn under Peter Koepke, implementing a version of homotopy type theory as an Isabelle object logic for my masters thesis. My bachelors thesis at the Australian National University under Scott Morrison was on quantum algebra, TQFTs, and an application to invariants of topological manifolds.