I'm a 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 proof assistants today. Things I'm currently working on include hybrid and alternative logical foundations in Isabelle, as well as proof automation for Coq and the ssreflect library. In general, I ponder how to make formal systems simple and powerful enough to become daily tools for mathematicians and computer scientists alike.

Previously, 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`

.