Publications

Quantum Programming

[1] Mingsheng Ying, Li Zhou, Yangjia Li, and Yuan Feng. A proof system for disjoint parallel quantum programs. Theor. Comput. Sci., 897:164–184, 2022. [ DOI | http ] Distinguished Paper Award at LICS 2022
[2] Yuxiang Peng, Mingsheng Ying, and Xiaodi Wu. Algebraic reasoning of quantum programs via non-idempotent kleene algebra. In PLDI '22: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, pages 657–670. ACM, 2022. [ DOI | http ]
[3] Junyi Liu, Li Zhou, Gilles Barthe, and Mingsheng Ying. Quantum weakest preconditions for reasoning about expected runtimes of quantum programs. In LICS '22: 37th Annual ACM/IEEE Symposium on Logic in Computer Science, pages 4:1–4:13. ACM, 2022. [ DOI | http ]
[4] Li Zhou, Gilles Barthe, Justin Hsu, Mingsheng Ying, and Nengkun Yu. A quantum interpretation of bunched logic & quantum separation logic. In 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, pages 1–14. IEEE, 2021. [ DOI | http ]
[5] Gilles Barthe, Justin Hsu, Mingsheng Ying, Nengkun Yu, and Li Zhou. Relational proofs for quantum programs. Proc. ACM Program. Lang., 4(POPL):21:1–21:29, 2020. [ DOI | http ]
[6] Gushu Li, Li Zhou, Nengkun Yu, Yufei Ding, Mingsheng Ying, and Yuan Xie. Projection-based runtime assertions for testing and debugging quantum programs. Proc. ACM Program. Lang., 4(OOPSLA):150:1–150:29, 2020. [ DOI | http ] Distinguished Paper Award at OOPSLA 2020
[7] Li Zhou, Nengkun Yu, and Mingsheng Ying. An applied quantum hoare logic. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019, pages 1149–1162. ACM, 2019. [ DOI | http ]
[8] Junyi Liu, Bohua Zhan, Shuling Wang, Shenggang Ying, Tao Liu, Yangjia Li, Mingsheng Ying, and Naijun Zhan. Formal verification of quantum algorithms using quantum hoare logic. In Computer Aided Verification - 31st International Conference, CAV 2019, volume 11562 of Lecture Notes in Computer Science, pages 187–207. Springer, 2019. [ DOI | http ]
[9] Shih-Han Hung, Kesha Hietala, Shaopeng Zhu, Mingsheng Ying, Michael Hicks, and Xiaodi Wu. Quantitative robustness analysis of quantum programs. Proc. ACM Program. Lang., 3(POPL):31:1–31:29, 2019. [ DOI | http ]
[10] Mingsheng Ying. Toward automatic verification of quantum programs. Formal Aspects Comput., 31(1):3–25, 2019. [ DOI | http ]
[11] Junyi Liu, Bohua Zhan, Shuling Wang, Shenggang Ying, Tao Liu, Yangjia Li, Mingsheng Ying, and Naijun Zhan. Quantum hoare logic. Arch. Formal Proofs, 2019, 2019. [ .html ]
[12] Yangjia Li and Mingsheng Ying. Algorithmic analysis of termination problems for quantum programs. Proc. ACM Program. Lang., 2(POPL):35:1–35:29, 2018. [ DOI | http ]
[13] Mingsheng Ying, Shenggang Ying, and Xiaodi Wu. Invariants of quantum programs: characterisations and generation. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, pages 818–832. ACM, 2017. [ DOI | http ]
[14] Yangjia Li, Nengkun Yu, and Mingsheng Ying. Termination of nondeterministic quantum programs. Acta Informatica, 51(1):1–24, 2014. [ DOI | http ]
[15] Mingsheng Ying, Nengkun Yu, Yuan Feng, and Runyao Duan. Verification of quantum programs. Sci. Comput. Program., 78(9):1679–1700, 2013. [ DOI | http ]
[16] Mingsheng Ying and Yuan Feng. A flowchart language for quantum programming. IEEE Trans. Software Eng., 37(4):466–485, 2011. [ DOI | http ]
[17] Mingsheng Ying. Floyd-hoare logic for quantum programs. ACM Trans. Program. Lang. Syst., 33(6):19:1–19:49, 2011. [ DOI | http ]
[18] Mingsheng Ying and Yuan Feng. Quantum loop programs. Acta Informatica, 47(4):221–250, 2010. [ DOI | http ]
[19] Yuan Feng, Runyao Duan, Zheng-Feng Ji, and Mingsheng Ying. Proof rules for the correctness of quantum programs. Theor. Comput. Sci., 386(1-2):151–166, 2007. [ DOI | http ]

This file was generated by bibtex2html 1.99.