Practical Sized Typing for Coq. - Jonathan Chan 002; William J. Bowman (CoRR, 2019)

Is sized typing for Coq practical? - Jonathan Chan 002; Yufeng Li; William J. Bowman (J. Funct. Program., 2023)

Internalizing Indistinguishability with Dependent Types. - Yiyun Liu; Jonathan Chan 002; Jessica Shi 002; Stephanie Weirich (Proc. ACM Program. Lang., 2024)

Stratified Type Theory. - Jonathan Chan 002; Stephanie Weirich (ESOP (1), 2025)

Consistency of a Dependent Calculus of Indistinguishability. - Yiyun Liu; Jonathan Chan 002; Stephanie Weirich (Proc. ACM Program. Lang., 2025)

Bounded First-Class Universe Levels in Dependent Type Theory. - Jonathan Chan 002; Stephanie Weirich (CoRR, 2025)