Hi, I'm Josh! I'm a soon-to-be Masters graduate of the University of Bonn, where I study mathematics and computer science. The themes of my research interests center around making computers “understand” the human processes of logic and language well enough, so that they can be used to automate and augment such processes for the good of society.

My work has involved both the pure and the applied. Most recently I have been working on type theory and automated theorem proving, implementing a working version of homotopy type theory inside the interactive proof assistant Isabelle. Homotopy type theory is a recent approach to extending intuitionistic type theory that is able to natively encode important mathematical concepts such as “isomorphism-as-equality” and structures such as fundamental groups. Its promise lies in its potential to provide a highly mechanizable alternative foundation for large portions of mathematics, and much current research is focused on questions of how to automatically check and prove mathematical statements encoded inside it. I developed the Isabelle/HoTT object logic as a first attempt to bring support for homotopy type theory to the Isabelle prover.

I also worked in data mining and natural language processing at the Fraunhofer Institute for Intelligent Analysis and Information Systems, where I used probabilistic machine learning models to automatically detect topics in tweet corpora and classify tweets accordingly. It is well-known that posts on public social media frequently reflect events occurring in the vicinity of the post location, in near real-time. By automatically detecting and classifying such posts, we can quickly identify issues which may be of relevance to law enforcement or emergency and rescue services in much less time than would otherwise be needed by more traditional channels of information. My work in this area was part of the E2mC Project, a pilot project that aims to use social media to enhance the European Union's emergency and natural disaster response service.

Some other areas in which I am particularly interested are applications of AI to automated fact-checking, as well as the theory of quantum computation. Previously, I studied at the Australian National University Mathematical Sciences Institute, writing my Bachelors thesis in category theory and quantum algebra, applied to low-dimensional topological invariants.