Hi, I'm Josh.
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.
- Dependent types and softly-typed set theory for Isabelle.
- CoqHammer — a hammer system for Coq and the calculus of inductive constructions.
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.
- Mathematical Language and Practical Type Theory ·
Hausdorff Center for Mathematics · Feb 1–4
- Prague Inter-reasoning Workshop ·
Czech Technical University in Prague · Oct 16–20
- Proof and Computation autumn school ·
Herrsching · Sep 20–26
- Homotopy Type Theory 2019 ·
Carnegie Mellon University · Aug 7–10, 12–17
- Conference on Intelligent Computer Mathematics ·
Czech Technical University in Prague · Jul 8–12
- Artificial Intelligence and Theorem Proving ·
Obergurgl · Apr 7–12
- School and Workshop on Univalent Mathematics ·
University of Birmingham · Apr 1–5