Hi, I'm Josh.
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:
- 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