I'm a new Ph.D. student in the Computational Logic group of the University of Innsbruck in Austria.

For my day job I work on improving the state of interactive theorem provers today. I'm currently working on soft type systems and a set theoretic logic for Isabelle, as well as on proof automation for Coq and the ssreflect library. More generally, I ponder how to make formal proof systems simple and powerful enough to become daily tools for mathematicians and computer scientists alike.

Before this, I studied mathematics at the University of Bonn and the Australian National University. I still moonlight as a mathematician interested in mathematical logic, type theory, and univalent foundations.

If you'd like to get in touch, I can be reached at `hellojoshchen.io`

.