Equational reasoning about quantum protocols

Research output: Chapter in Book/Report/Conference proceedingConference contribution


Communicating Quantum Processes (CQP) is a quantum process calculus that applies formal techniques from classical computer science to concurrent and communicating systems that combine quantum and classical computation. By employing the theory of behavioural equivalence between processes, it is possible to verify the correctness of a system in CQP. The equational theory of CQP helps us to analyse quantum systems by reducing the need to explicitly construct bisimulation relations. We add three new equational axioms to the existing equational theory of CQP, which helps us to analyse various quantum protocols by proving that the implementation and specification are equivalent. We summarise the necessary theory and demonstrate its application in the analysis of quantum secret sharing. Also, we illustrate the approach by verifying other interesting and important practical quantum protocols such as superdense coding, quantum error correction and remote CNOT.
Original languageEnglish
Title of host publicationReversible Computation
Subtitle of host publication7th International Conference, RC 2015, Grenoble, France, July 16-17, 2015, Proceedings
EditorsJean Krivine, Jean-Bernard Stefani
Number of pages16
ISBN (Electronic)978-3-319-20860-2
ISBN (Print)978-3-319-20859-6
Publication statusPublished - 2015

Publication series

NameLecture Notes in Computer Science
PublisherSpringer International Publishing
ISSN (Print)0302-9743


Dive into the research topics of 'Equational reasoning about quantum protocols'. Together they form a unique fingerprint.

Cite this