We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:


Current browse context:


Change to browse by:

References & Citations


(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Quantum Physics

Title: Verification of Distributed Quantum Programs

Abstract: Distributed quantum systems and especially the Quantum Internet have the ever-increasing potential to fully demonstrate the power of quantum computation. This is particularly true given that developing a general-purpose quantum computer is much more difficult than connecting many small quantum devices. One major challenge of implementing distributed quantum systems is programming them and verifying their correctness. In this paper, we propose a CSP-like distributed programming language to facilitate the specification and verification of such systems. After presenting its operational and denotational semantics, we develop a Hoare-style logic for distributed quantum programs and establish its soundness and (relative) completeness with respect to both partial and total correctness. The effectiveness of the logic is demonstrated by its applications in the verification of quantum teleportation and local implementation of non-local CNOT gates, two important algorithms widely used in distributed quantum systems.
Comments: arXiv admin note: text overlap with arXiv:2008.06812
Subjects: Quantum Physics (quant-ph); Logic in Computer Science (cs.LO)
Cite as: arXiv:2104.14796 [quant-ph]
  (or arXiv:2104.14796v1 [quant-ph] for this version)

Submission history

From: Yuan Feng [view email]
[v1] Fri, 30 Apr 2021 07:23:55 GMT (110kb,D)

Link back to: arXiv, form interface, contact.