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

For my day job I work on improving the state of interactive theorem provers today. I'm currently working on soft type systems for set theoretic and generic logics in 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.

I moonlight as a mathematician interested in type theory, mathematical logic, and formalization.

If you'd like to get in touch, I'm reachable at `hello@joshchen.io`

.