Foundationally Sound Annotation Verifier via Control Flow Splitting. - Litao Zhou 001 (SPLASH Companion, 2022)

Recursive Subtyping for All. - Litao Zhou 001; Yaoda Zhou; Bruno C. d. S. Oliveira (Proc. ACM Program. Lang., 2023)

Full Iso-Recursive Types. - Litao Zhou 001; Qianyong Wan; Bruno C. d. S. Oliveira (Proc. ACM Program. Lang., 2024)

VST-A: A Foundationally Sound Annotation Verifier. - Litao Zhou 001; Jianxing Qin; Qinshi Wang; Andrew W. Appel; Qinxiang Cao (Proc. ACM Program. Lang., 2024)

Recursive subtyping for all. - Litao Zhou 001; Yaoda Zhou; Qianyong Wan; Bruno C. d. S. Oliveira (J. Funct. Program., 2025)

QuickSub: Efficient Iso-Recursive Subtyping. - Litao Zhou 001; Bruno C. d. S. Oliveira (Proc. ACM Program. Lang., 2025)