Lexos 2017: building reliable software in python. - Cheng Zhang 026; Weiqi Feng; Emma Steffens; Alvaro de Landaluce; Scott Kleinman; Mark D. LeBlanc (J. Comput. Sci. Coll., 2018)

On incorrectness logic and Kleene algebra with top and tests. - Cheng Zhang 026; Arthur Azevedo de Amorim; Marco Gaboardi (Proc. ACM Program. Lang., 2022)

A Dependently Typed Language with Dynamic Equality. - Mark Lemay; Qiancheng Fu; William Blair; Cheng Zhang 026; Hongwei Xi 001 (TyDe@ICFP, 2023)

Domain Reasoning in TopKAT. - Cheng Zhang 026; Arthur Azevedo de Amorim; Marco Gaboardi (ICALP, 2024)

Kleene Algebra with Commutativity Conditions Is Undecidable. - Arthur Azevedo de Amorim; Cheng Zhang 026; Marco Gaboardi (CSL, 2025)

CF-GKAT: Efficient Validation of Control-Flow Transformations. - Cheng Zhang 026; Tobias Kappé; David E. Narváez; Nico Naus (Proc. ACM Program. Lang., 2025)