Programming methodologies and technologies are a central theme of computer science. Due to the essential differences between the nature of the classical world and that of the quantum world, today’s programming techniques are not suited to quantum computers. Furthermore, as human intuition is poorly adapted to the quantum world, design and implementation errors will creep into complex quantum software and cryptographic systems. Quantum programming and verification group at QSI investigates how to program a future quantum computer, and in particular, how quantum features such as superposition and entanglement can be fully exploited in the new programming models. This group also aims to develop formal methods and automatic tools for verification of quantum programs and cryptographic protocols.
Key Members: Prof Runyao Duan, Prof Mingsheng Ying
Models of quantum programming
We aim at discovering new programming models that can properly exploit the unique power of quantum computers. One challenge in quantum programming research is to understand control flow of quantum programs, quantum recursion, and concurrency in quantum computation.
Verification of quantum programs
Programming is error prone. It will be even worse to program a quantum computer. We try to build a logical foundation for verification of quantum programs, and to develop a chain of verification techniques including model-checking quantum systems.
Based on our theoretical research, we are designing and implementing a set of automatic tools for verifying correctness of quantum programs and security of quantum cryptographic protocols, including model-checker for quantum Markov chains, theorem prover for quantum programs, and bisimulation checker and emulation tool for quantum communicating processes.
- Mingsheng Ying, Shenggang Ying, and Xiaodi Wu. Invariants of quantum programs: characterisations and generation. POPL 2017.
- Mingsheng Ying. Foundations of quantum programming. Elsevier - Morgan Kaufmann (2016).
- Yuan Feng, Nengkun Yu, and Mingsheng Ying. Model checking quantum Markov chains. J. Comput. Syst. Sci. (2013).
- Yuan Feng, Runyao Duan, and Mingsheng Ying. Bisimulation for quantum processes. ACM Trans. Program. Lang. Syst. (2012). (Earlier version: POPL 2011).
- Mingsheng Ying. Floyd-Hoare logic for quantum programs. ACM Trans. Program. Lang. Syst (2011).