A proof system for disjoint parallel quantum programs

In this paper, we define the operational and denotational semantics of a special class of parallel quantum programs, namely disjoint parallel quantum programs. Based on them, a proof system for reasoning about disjoint parallel quantum programs is developed, which is (relatively) complete even when entanglement between different processes appears in the preconditions and postconditions.

Authors

• Mingsheng Ying
• Li Zhou TAO Technology, Alibaba Group
• Yangjia Li
• Yuan Feng

Keywords

• Quantum programming
• Quantum Hoare logic
• Parallel programs
• Entanglement