A Coq Library of Sets for Teaching Denotational Semantics. - Qinxiang Cao; Xiwei Wu; Yalun Liang (ThEdu@CADE, 2023)

CompCertOC: Verified Compositional Compilation of Multi-threaded Programs with Shared Stacks. - Ling Zhang; Yuting Wang 001; Yalun Liang; Zhong Shao 001 (Proc. ACM Program. Lang., 2025)

CompCertOC: Verified Compositional Compilation of Multi-Threaded Programs with Shared Stacks. - Ling Zhang; Yuting Wang 001; Yalun Liang; Zhong Shao 001 (Zenodo, 2025)