Undecidability of $D_{<: }$ and Its Decidable Fragments. - Jason Z. S. Hu; Ondrej Lhoták (CoRR, 2019)

Proof-relevant Category Theory in Agda. - Jason Z. S. Hu; Jacques Carette (CoRR, 2020)

Undecidability of d<: and its decidable fragments. - Jason Z. S. Hu; Ondrej Lhoták (Proc. ACM Program. Lang., 2020)

Formalizing category theory in Agda. - Jason Z. S. Hu; Jacques Carette (CPP, 2021)

Internal Category with Families in Presheaves. - Jason Z. S. Hu (CoRR, 2021)

An Investigation of Kripke-style Modal Type Theories. - Jason Z. S. Hu; Brigitte Pientka (CoRR, 2022)

A Categorical Normalization Proof for the Modal Lambda-Calculus. - Jason Z. S. Hu; Brigitte Pientka (MFPS, 2022)

A Category Theoretic View of Contextual Types: From Simple Types to Dependent Types. - Jason Z. S. Hu; Brigitte Pientka; Ulrich Schöpp (ACM Trans. Comput. Log., 2022)

Layered Modal Type Theories. - Jason Z. S. Hu; Brigitte Pientka (CoRR, 2023)

Normalization by evaluation for modal dependent type theory. - Jason Z. S. Hu; Junyoung Jang 001; Brigitte Pientka (J. Funct. Program., 2023)

Layered Modal Type Theory - Where Meta-programming Meets Intensional Analysis. - Jason Z. S. Hu; Brigitte Pientka (ESOP (1), 2024)

DeLaM: A Dependent Layered Modal Type Theory for Meta-programming. - Jason Z. S. Hu; Brigitte Pientka (CoRR, 2024)

A Layered Approach to Intensional Analysis in Type Theory. - Jason Z. S. Hu; Brigitte Pientka (ACM Trans. Program. Lang. Syst., 2024)

A Dependent Type Theory for Meta-programming with Intensional Analysis. - Jason Z. S. Hu; Brigitte Pientka (Proc. ACM Program. Lang., 2025)