Thanks to the rapid progress and growing complexity of quantum algorithms, correctness of quantum programs has become a major concern. Pioneering research over the past years has proposed various approaches to formally verify quantum programs using …
We investigate the algebraic reasoning of quantum programs inspired by the success of classical program analysis based on Kleene algebra. One prominent example of such is the famous Kleene Algebra with Tests (KAT), which has furnished both …
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 …