Differential Privacy in Quantum Computation. - Li Zhou 013; Mingsheng Ying (CSF, 2017)

Q|SI〉: A Quantum Programming Environment. - Shusen Liu 002; Xin Wang 022; Li Zhou 013; Ji Guan 001; Yinan Li; Yang He; Runyao Duan; Mingsheng Ying (CoRR, 2017)

Q|SI⟩ : A Quantum Programming Environment. - Shusen Liu 002; Xin Wang 022; Li Zhou 013; Ji Guan 001; Yinan Li; Yang He; Runyao Duan; Mingsheng Ying (Symposium on Real-Time and Hybrid Systems, 2018)

Quantum Coupling and Strassen Theorem. - Li Zhou 013; Shenggang Ying; Nengkun Yu; Mingsheng Ying (CoRR, 2018)

An applied quantum Hoare logic. - Li Zhou 013; Nengkun Yu; Mingsheng Ying (PLDI, 2019)

Coupling Techniques for Reasoning about Quantum Programs. - Gilles Barthe; Justin Hsu; Mingsheng Ying; Nengkun Yu; Li Zhou 013 (CoRR, 2019)

Protocols for Packet Quantum Network Intercommunication. - Nengkun Yu; Ching-Yi Lai; Li Zhou 013 (CoRR, 2019)

Expected Runtime of Quantum Programs. - Junyi Liu 002; Li Zhou 013; Mingsheng Ying (CoRR, 2019)

Poq: Projection-based Runtime Assertions for Debugging on a Quantum Computer. - Gushu Li; Li Zhou 013; Nengkun Yu; Yufei Ding 001; Mingsheng Ying; Yuan Xie 001 (CoRR, 2019)

Relational proofs for quantum programs. - Gilles Barthe; Justin Hsu; Mingsheng Ying; Nengkun Yu; Li Zhou 013 (Proc. ACM Program. Lang., 2020)

Projection-based runtime assertions for testing and debugging Quantum programs. - Gushu Li; Li Zhou 013; Nengkun Yu; Yufei Ding 001; Mingsheng Ying; Yuan Xie 001 (Proc. ACM Program. Lang., 2020)

Strassen's theorem for quantum couplings. - Li Zhou 013; Shenggang Ying; Nengkun Yu; Mingsheng Ying (Theor. Comput. Sci., 2020)

A Quantum Interpretation of Bunched Logic & Quantum Separation Logic. - Li Zhou 013; Gilles Barthe; Justin Hsu; Mingsheng Ying; Nengkun Yu (LICS, 2021)

EasyPQC: Verifying Post-Quantum Cryptography. - Manuel Barbosa; Gilles Barthe; Xiong Fan; Benjamin Grégoire; Shih-Han Hung; Jonathan Katz; Pierre-Yves Strub; Xiaodi Wu 001; Li Zhou 013 (IACR Cryptol. ePrint Arch., 2021)

When is the Chernoff Exponent for Quantum Operations Finite? - Nengkun Yu; Li Zhou 013 (IEEE Trans. Inf. Theory, 2021)

A proof system for disjoint parallel quantum programs. - Mingsheng Ying; Li Zhou 013; Yangjia Li; Yuan Feng 001 (Theor. Comput. Sci., 2022)

Comments on and Corrections to "When Is the Chernoff Exponent for Quantum Operations Finite?". - Nengkun Yu; Li Zhou 013 (IEEE Trans. Inf. Theory, 2022)

Refinement calculus of quantum programs with projective assertions. - Yuan Feng 001; Li Zhou 013; Yingte Xu (CoRR, 2023)

CoqQ: Foundational Verification of Quantum Programs. - Li Zhou 013; Gilles Barthe; Pierre-Yves Strub; Junyi Liu 002; Mingsheng Ying (Proc. ACM Program. Lang., 2023)

Laws of Quantum Programming. - Mingsheng Ying; Li Zhou 013; Gilles Barthe (CoRR, 2024)

D-Hammer: Efficient Equational Reasoning for Labelled Dirac Notation. - Yingte Xu; Li Zhou 013; Gilles Barthe (CAV (4), 2025)

Efficient Formal Verification of Quantum Error Correcting Programs. - Qifan Huang; Li Zhou 013; Wang Fang 001; Mengyu Zhao; Mingsheng Ying (Proc. ACM Program. Lang., 2025)

Automating Equational Proofs in Dirac Notation. - Yingte Xu; Gilles Barthe; Li Zhou 013 (Proc. ACM Program. Lang., 2025)

Complete Quantum Relational Hoare Logics from Optimal Transport Duality. - Gilles Barthe; Minbo Gao; Theo Wang; Li Zhou 013 (CoRR, 2025)

Quantum Weakest Preconditions for Reasoning about Expected Runtimes of Quantum Programs. - Junyi Liu 002; Li Zhou 013; Gilles Barthe; Mingsheng Ying (J. ACM, 2025)