Li Zhou

37 papers A* 5A 1Journal 28Unranked 2
YearRankTypeTitle / Venue / Authors
2026 J jnl
An Expressive Assertion Language for Quantum Programs.
Proc. ACM Program. Lang.
Bonan Su, Yuan Feng, Mingsheng Ying, Li Zhou
2026 — conf
Borrowing Dirty Qubits in Quantum Programs.
ASPLOS (2)
Bonan Su, Li Zhou, Yuan Feng, Mingsheng Ying
2025 J jnl
A Duality Theorem for Classical-Quantum States with Applications to Complete Relational Program Logics.
CoRR
Gilles Barthe, Minbo Gao, Jam Kabeer Ali Khan, Matthijs Muis, Ivan Renison, Keiya Sakabe, Michael Walter, Yingte Xu, Li Zhou
2025 J jnl
Automating Equational Proofs in Dirac Notation.
Proc. ACM Program. Lang.
Yingte Xu, Gilles Barthe, Li Zhou
2025 J jnl
Borrowing Dirty Qubits in Quantum Programs.
CoRR
Bonan Su, Li Zhou, Yuan Feng, Mingsheng Ying
2025 A* conf
Complete Quantum Relational Hoare Logics from Optimal Transport Duality.
LICS
Gilles Barthe, Minbo Gao, Theo Wang, Li Zhou
2025 J jnl
Complete Quantum Relational Hoare Logics from Optimal Transport Duality.
CoRR
Gilles Barthe, Minbo Gao, Theo Wang, Li Zhou
2025 — conf
D-Hammer: Efficient Equational Reasoning for Labelled Dirac Notation.
CAV (4)
Yingte Xu, Li Zhou, Gilles Barthe
2025 J jnl
D-Hammer: Efficient Equational Reasoning for Labelled Dirac Notation.
CoRR
Yingte Xu, Li Zhou, Gilles Barthe
2025 J jnl
Efficient Formal Verification of Quantum Error Correcting Programs.
CoRR
Qifan Huang, Li Zhou, Wang Fang, Mengyu Zhao, Mingsheng Ying
2025 J jnl
Efficient Formal Verification of Quantum Error Correcting Programs.
Proc. ACM Program. Lang.
Qifan Huang, Li Zhou, Wang Fang, Mengyu Zhao, Mingsheng Ying
2025 J jnl
Quantum Weakest Preconditions for Reasoning about Expected Runtimes of Quantum Programs.
J. ACM
Junyi Liu, Li Zhou, Gilles Barthe, Mingsheng Ying
2024 J jnl
Automating Equational Proofs in Dirac Notation.
CoRR
Yingte Xu, Gilles Barthe, Li Zhou
2024 J jnl
Laws of Quantum Programming.
CoRR
Mingsheng Ying, Li Zhou, Gilles Barthe
2023 J jnl
CoqQ: Foundational Verification of Quantum Programs.
Proc. ACM Program. Lang.
Li Zhou, Gilles Barthe, Pierre-Yves Strub, Junyi Liu, Mingsheng Ying
2023 J jnl
Refinement calculus of quantum programs with projective assertions.
CoRR
Yuan Feng, Li Zhou, Yingte Xu
2022 J jnl
A proof system for disjoint parallel quantum programs.
Theor. Comput. Sci.
Mingsheng Ying, Li Zhou, Yangjia Li, Yuan Feng
2022 J jnl
Comments on and Corrections to "When Is the Chernoff Exponent for Quantum Operations Finite?".
IEEE Trans. Inf. Theory
Nengkun Yu, Li Zhou
2022 J jnl
CoqQ: Foundational Verification of Quantum Programs.
CoRR
Li Zhou, Gilles Barthe, Pierre-Yves Strub, Junyi Liu, Mingsheng Ying
2022 A* conf
Quantum Weakest Preconditions for Reasoning about Expected Runtimes of Quantum Programs.
LICS
Junyi Liu, Li Zhou, Gilles Barthe, Mingsheng Ying
2021 A* conf
A Quantum Interpretation of Bunched Logic & Quantum Separation Logic.
LICS
Li Zhou, Gilles Barthe, Justin Hsu, Mingsheng Ying, Nengkun Yu
2021 J jnl
A Quantum Interpretation of Bunched Logic for Quantum Separation Logic.
CoRR
Li Zhou, Gilles Barthe, Justin Hsu, Mingsheng Ying, Nengkun Yu
2021 A* conf
EasyPQC: Verifying Post-Quantum Cryptography.
CCS
Manuel Barbosa, Gilles Barthe, Xiong Fan, Benjamin Grégoire, Shih-Han Hung, Jonathan Katz, Pierre-Yves Strub, Xiaodi Wu, Li Zhou
2021 J jnl
EasyPQC: Verifying Post-Quantum Cryptography.
IACR Cryptol. ePrint Arch.
Manuel Barbosa, Gilles Barthe, Xiong Fan, Benjamin Grégoire, Shih-Han Hung, Jonathan Katz, Pierre-Yves Strub, Xiaodi Wu, Li Zhou
2021 J jnl
When is the Chernoff Exponent for Quantum Operations Finite?
IEEE Trans. Inf. Theory
Nengkun Yu, Li Zhou
2020 J jnl
Projection-based runtime assertions for testing and debugging Quantum programs.
Proc. ACM Program. Lang.
Gushu Li, Li Zhou, Nengkun Yu, Yufei Ding, Mingsheng Ying, Yuan Xie
2020 J jnl
Relational proofs for quantum programs.
Proc. ACM Program. Lang.
Gilles Barthe, Justin Hsu, Mingsheng Ying, Nengkun Yu, Li Zhou
2020 J jnl
Strassen's theorem for quantum couplings.
Theor. Comput. Sci.
Li Zhou, Shenggang Ying, Nengkun Yu, Mingsheng Ying
2019 A* conf
An applied quantum Hoare logic.
PLDI
Li Zhou, Nengkun Yu, Mingsheng Ying
2019 J jnl
Coupling Techniques for Reasoning about Quantum Programs.
CoRR
Gilles Barthe, Justin Hsu, Mingsheng Ying, Nengkun Yu, Li Zhou
2019 J jnl
Expected Runtime of Quantum Programs.
CoRR
Junyi Liu, Li Zhou, Mingsheng Ying
2019 J jnl
Poq: Projection-based Runtime Assertions for Debugging on a Quantum Computer.
CoRR
Gushu Li, Li Zhou, Nengkun Yu, Yufei Ding, Mingsheng Ying, Yuan Xie
2019 J jnl
Protocols for Packet Quantum Network Intercommunication.
CoRR
Nengkun Yu, Ching-Yi Lai, Li Zhou
2018 J jnl
Quantum Coupling and Strassen Theorem.
CoRR
Li Zhou, Shenggang Ying, Nengkun Yu, Mingsheng Ying
2018 — ch.
Q|SI⟩ : A Quantum Programming Environment.
Symposium on Real-Time and Hybrid Systems
Shusen Liu, Xin Wang, Li Zhou, Ji Guan, Yinan Li, Yang He, Runyao Duan, Mingsheng Ying
2017 A conf
Differential Privacy in Quantum Computation.
CSF
Li Zhou, Mingsheng Ying
2017 J jnl
Q|SI〉: A Quantum Programming Environment.
CoRR
Shusen Liu, Xin Wang, Li Zhou, Ji Guan, Yinan Li, Yang He, Runyao Duan, Mingsheng Ying