I’m a PhD candidate in computer science at the Functional Programming Lab of the University of Nottingham, advised by Nicolai Kraus.
My current research involves the study of programming languages and logics known as homotopy type theories, and how we can use them to express, reason about, and compute with higher categorical structures that arise in mathematics, software, and physical systems.
Previously, I worked in machine learning and natural language processing at the Knowledge Discovery group at Fraunhofer IAIS, and on formalization and proof assistants at the Computational Logic group of the University of Innsbruck. Prior to that I majored in mathematics at the University of Bonn and the Australian National University.
Categories as Semicategories with Identities. With Tom de Jong, Nicolai Kraus and Stiéphen Pradal. 29th International Conference on Types for Proofs and Programs (TYPES). Jun 2023. Extended abstract. Valencia. URL: https://types2023.webs.upv.es/TYPES2023.pdf.
Semisimplicial Types in Internal Categories with Families. With Nicolai Kraus. 27th International Conference on Types for Proofs and Programs (TYPES). Jun 2021. Extended abstract. Leiden (virtual). URL: https://types21.liacs.nl/download/semisimplicial-types-in-internal-categories-with-families.
Homotopy Type Theory in Isabelle. 12th International Conference on Interactive Theorem Proving (ITP). Jun 2021. Rome (virtual). URL: https://doi.org/10.4230/LIPIcs.ITP.2021.12.
An Implementation of Homotopy Type Theory in Isabelle. Sep 2018. Masters thesis. Type theory, mathematical logic and proof assistants. University of Bonn. URL: https://arxiv.org/abs/1911.00399.
The Temperley-Lieb categories and skein modules. May 2014. Bachelors (Honours) thesis. Diagrammatic quantum algebra and category theory. The Australian National University. URL: https://arxiv.org/abs/1502.06845.
Miscellaneous technical writing.
Semantic (aka soft) types. Nov 2019. Extended abstract. University of Innsbruck. URL: https://joshchen.io/pdf/soft-types-abstract.pdf.
Computational Fact-Checking. Jul 2017. Technical report. University of Bonn. URL: https://joshchen.io/pdf/computational-fact-checking-report.pdf.
A pre-introduction to homotopy type theory. 2017. Seminar notes. University of Bonn. URL: https://joshchen.io/pdf/hott-preintro-notes.pdf.
On internal models of type theory and Reedy fibrant diagrams. YaMCATS meeting 29. Dec 2022. Invited talk. University of Manchester.
Abstract
A current major obstruction to the use of standard homotopy type theory as a language for ∞-category theory is the longstanding open problem of constructing semisimplicial objects in the universe of types. Numerous attempts and a number of clever proposals have all eventually run up against essentially the same wall: we have not yet found a way of internalizing the tower of coherence conditions required for a correct definition of the [n]-matching type for arbitrary n.
Seemingly distinct is the open problem of whether or not the universe type of HoTT models HoTT itself, or, phrased alternatively, if one may find a suitable notion of “model of type theory” that classes both the syntactic model and the so-called “standard model” of the universe as examples.
In joint work with Nicolai Kraus we suggest the following line of investigation: taking HoTT as our ambient metatheory, we consider internal models of type theory and construct semisimplicial types (and more general Reedy fibrant diagrams) in them. The case when the internal model is set-truncated may be viewed as an inversion of the two-level type theoretic setting, and already here the construction of diagrams requires somewhat more work than in 2LTT. One aim of this program is to later relax the truncation levels in order to yield higher internal models of type theory with proof-relevant judgmental equality, and to move our constructions into these new settings. Along the way, we prove half of a conjectured equivalence between the two open problems mentioned previously: HoTT models its own metatheory only if semisimplicial types are constructible; and also speculate on possible formulations of the coherence problem for semisimplicial types.
Semisimplicial Types in Internal Categories with Families. 27th International Conference on Types for Proofs and Programs (TYPES). Jun 2021. Leiden (virtual). URL: https://joshchen.io/media/semisimplicial-types-in-internal-categories-with-families.mp4 Slides: https://joshchen.io/pdf/types-2021-slides.pdf.
Homotopy Type Theory in Isabelle. 12th International Conference on Interactive Theorem Proving (ITP). Jun 2021. Rome (virtual). URL: https://youtu.be/fGnIdt_jPfA?t=4630 Slides: https://joshchen.io/pdf/itp-2021-slides.pdf.
Dependent Types in Isabelle. 4th Prague Inter-Reasoning Workshop. Oct 2019. Czech Technical University.
Isabelle/HoTT. Jul 2019. Seminar talk. Chair for Logic and Verification, Technical University of Munich.
Hybrid and Alternative Logics in Isabelle: Isabelle/Set. Conference on Intelligent Computer Mathematics. Jul 2019. Doctoral program. Prague. Slides: https://joshchen.io/pdf/cicm-2019-slides.pdf.
Semantic Types. May 2019. Seminar talk. Computational Logic research seminar, University of Innsbruck. Slides: https://joshchen.io/pdf/semantic-types-slides.pdf.
What is Mathematics? 2014. Outreach talk, ANU Open Day. The Australian National University.
An Introduction to Topological Quantum Field Theory. Australian Mathematical Sciences Student Conference. 2014. The University of Newcastle, Australia.
The Temperley-Lieb categories and Turaev-Viro skein modules. ANU MSI Honours Conference. 2014. The Australian National University.
I have been tutor and/or teaching assistant for the following courses.
Introduction to formal reasoning Formal logic in the Lean proof assistant. 2nd year Bachelors course. University of Nottingham.
Introductory Haskell 1st year Bachelors course. University of Nottingham.
Mathematics and applications 1st year Bachelors course. The Australian National University.
Mathematics and applications 1st year Bachelors course. University of Canterbury.
Dependently typed and set-theoretic foundations for formalized mathematics in Isabelle University of Innsbruck.
Investigated dependently typed and set theoretic logics, infrastructure and tools for the formalization of mathematics in the Isabelle proof assistant, under the ERC-funded “SMART” project at the Computational Logic group.
Machine learning and natural language processing for Copernicus EMS Fraunhofer Institute for Intelligent Analysis and Information Systems.
Worked in the Knowledge Discovery group, implenting and applying probabilistic models to analyze and classify topics in Twitter data corpora. Implemented targeted topic models in Java, and used Python for natural language processing of Twitter and Facebook data. This work was part of the European Union’s E2mC project, a pilot project that used publicly available social media data for real-time support of its Copernicus emergency management service.
Enumeration and visualization of planar trivalent graphs The Australian National University.
Developed and implemented algorithms in Scala to count and automatically draw certain classes of planar graphs. Part of quantum algebra research investigating subfactors and planar algebras.
Temperley-Lieb categories and skein modules The Australian National University.
Final year Honours research thesis in category theory, quantum algebra, and applications to low-dimensional topological invariants.
Integer houses in cyclotomic fields The Australian National University.
Summer research scholarship. Investigated questions concerning the dimensions of objects in fusion categories using Wolfram Mathematica.
Ph.D. in Computer Science University of Nottingham.
Advisor: Nicolai Kraus.
Masters in Mathematics University of Bonn.
German GPA 1.9. Advisor: Peter Koepke.
B.Sc. (Hons) in Mathematics The Australian National University.
GPA 80%. First Class Honours. Advisor: Scott Morrison.
B.Sc. in Mathematics University of Canterbury.
GPA 8.64/9.00. Dean’s Congratulations.