Communicating quantum processes

DOI10.1145/1040305.1040318zbMATH Open1369.68207arXivquant-ph/0409052OpenAlexW2064622659WikidataQ130929367 ScholiaQ130929367MaRDI QIDQ5276142FDOQ5276142

Authors: Rajagopal Nagarajan, Simon J. Gay 

Publication date: 14 July 2017

Published in: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Abstract: We define a language CQP (Communicating Quantum Processes) for modelling systems which combine quantum and classical communication and computation. CQP combines the communication primitives of the pi-calculus with primitives for measurement and transformation of quantum state; in particular, quantum bits (qubits) can be transmitted from process to process along communication channels. CQP has a static type system which classifies channels, distinguishes between quantum and classical data, and controls the use of quantum state. We formally define the syntax, operational semantics and type system of CQP, prove that the semantics preserves typing, and prove that typing guarantees that each qubit is owned by a unique process within a system. We illustrate CQP by defining models of several quantum communication systems, and outline our plans for using CQP as the foundation for formal analysis and verification of combined quantum and classical systems.

Full work available at URL: https://arxiv.org/abs/quant-ph/0409052

Recommendations

• Types and typechecking for Communicating Quantum Processes
• Equational reasoning about quantum protocols
• An algebra of quantum processes
• Probabilistic bisimulations for quantum processes
• scientific article; zbMATH DE number 1612487

zbMATH Keywords

verificationtypessemanticsquantum communicationquantum computingformal language

Mathematics Subject Classification ID

Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Quantum computation (81P68) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Cited In (30)

• Branching bisimulation semantics for quantum processes
• Analysis of a quantum error correcting code using quantum process calculus
• Types and typechecking for Communicating Quantum Processes
• Interaction in Quantum Communication
• Formalization \textit{of} quantum protocols using Coq
• Model-checking linear-time properties of quantum systems
• Probabilistic bisimulations for quantum processes
• An axiomatization for quantum processes to unifying quantum and classical computing
• Entanglement in quantum process algebra
• Formal verification for KMB09 protocol
• Probabilistic process algebra to unifying quantum and classical computing in closed systems
• Verifying quantum communication protocols with ground bisimulation
• Distributed measurement-based quantum computation
• A process algebra for reasoning about quantum security
• Encodability criteria for quantum based systems
• Termination of nondeterministic quantum programs
• Distributed quantum programming
• Equational reasoning about quantum protocols
• On well-founded and recursive coalgebras
• Quantum patterns and types for entanglement and separability
• Describing and animating quantum protocols
• Simulating and compiling code for the sequential quantum random access machine
• Encodability criteria for quantum based systems
• Symbolic bisimulation for quantum processes
• Techniques for Formal Modelling and Analysis of Quantum Systems
• Bisimulations for probabilistic and quantum processes (invited paper)
• Quantum process algebra with priorities
• Classical knowledge for quantum cryptographic reasoning
• Quantum arrows in Haskell
• Quantum communication protocols as a benchmark for programmable quantum computers

This page was built for publication: Communicating quantum processes

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5276142)