article

Communicating quantum processes

Authors:

Rajagopal NagarajanAuthors Info & Claims

ACM SIGPLAN Notices, Volume 40, Issue 1

Pages 145 - 157

https://doi.org/10.1145/1047659.1040318

Published: 12 January 2005 Publication History

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.

References

[1]

CWB-NC: www.cs.sunysb.edu/~cwb.

[2]

S. Abramsky and B. Coecke. A categorical semantics of quantum protocols. In Proceedings, Nineteenth Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, 2004.

Digital Library

[3]

C. H. Bennett and G. Brassard. Quantum Cryptography: Public-key Distribution and Coin Tossing. In Proceedings of the IEEE International Conference on Computer, Systems and Signal Processing, Bangalore, India, pages 175--179, 1984.

[4]

C. H. Bennett, G. Brassard, C. Crépeau, R. Jozsa, A. Peres, and W. K. Wootters. Teleporting an unknown quantum state via dual classical and Einstein-Podolsky-Rosen channels. Phys. Rev. Lett., 70:1895--1899, 1993.

[5]

D. Cazorla, F. Cuartero, V. Valero, F. L. Pelayo, and J. J. Pardo. Algebraic theory of probabilistic and nondeterministic processes. Journal of Logic and Algebraic Programming, 55:57--103, 2003.

[6]

H. de Riedmatten, I. Marcikic, W. Tittel, H. Zbinden, D. Collins, and N. Gisin. Long distance quantum teleportation in a quantum relay configuration. Phys. Rev. Lett., 92(4), 2004.

[7]

R. Ennals, R. Sharp, and A. Mycroft. Linear types for packet processing. In D. Schmidt, editor, ESOP 2004: Proceedings of the European Symposium on Programming, volume 2986 of Lecture Notes in Computer Science. Springer-Verlag, 2004.

[8]

J. Gruska. Quantum Computing. McGraw-Hill, 1999.

[9]

P. Jorrand and M. Lalire. A process-algebraic approach to concurrent and distributed quantum computation: operational semantics. In P. Selinger, editor, Proceedings of the 2nd International Workshop on Quantum Programming Languages, 2004. Also in Quantum Physics Archive: arXiv:quant-ph/0407005.

[10]

E. Knill. Conventions for quantum pseudocode. Technical Report LAUR-96-2724, Los Alamos National Laboratory, 1996.

[11]

N. Kobayashi, B. C. Pierce, and D. N. Turner. Linearity and the Pi-Calculus. ACM Transactions on Programming Languages and Systems, 21(5):914--947, September 1999.

Digital Library

[12]

M. Z. Kwiatkowska, G. Norman, and D. Parker. PRISM: Probabilistic symbolic model checker. In T. Field, P. Harrison, J. Bradley, and U. Harder, editors, Computer Performance Evaluation (TOOLS'02), pages 200--204. Springer-Verlag, 2002.

Digital Library

[13]

D. Mayers. Unconditional Security in Quantum Cryptography. Journal of the ACM, 48(3):351--406, May 2001.

Digital Library

[14]

D. A. Meyer. Quantum strategies. Physical Review Letters, 82(5), 1999.

[15]

R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes, I and II. Information and Computation, 100(1):1--77, September 1992.

Digital Library

[16]

R. Nagarajan and S. J. Gay. Formal verification of quantum protocols. Quantum Physics Archive: arXiv:quant-ph/0203086, March 2002.

[17]

M. A. Nielsen and I. L. Chuang. Quantum Computation and Quantum Information. Cambridge University Press, 2000.

Digital Library

[18]

B. Ömer. Quantum programming in QCL. Master's thesis, Technical University of Vienna, 2000.

[19]

N. Papanikolaou. Techniques for design and validation of quantum protocols. Master's thesis, University of Warwick, 2004.

[20]

B. C. Pierce and D. Sangiorgi. Typing and subtyping for mobile processes. Mathematical Structures in Computer Science, 6(5), 1996.

[21]

A. Poppe, A. Fedrizzi, T. Lorünser, O. Maurhardt, R. Ursin, H. R. Böhm, M. Peev, M. Suda, C. Kurtsiefer, H. Weinfurter, T. Jennewein, and A. Zeilinger. Practical quantum key distribution with polarization entangled photons. Quantum Physics Archive: arXiv:quant-ph/0404115, 2004.

[22]

E. G. Rieffel and W. Polak. An introduction to quantum computing for non-physicists. ACM Computing Surveys, 32(3):300--335, 2000.

Digital Library

[23]

P. Ryan, S. Schneider, M. Goldsmith, G. Lowe, and B. Roscoe. Modelling and Analysis of Security Protocols. Addison-Wesley, 2001.

Digital Library

[24]

J. W. Sanders and P. Zuliani. Quantum programming. In Mathematics of Program Construction, volume 1837 of Springer LNCS, 2000.

Digital Library

[25]

D. Sangiorgi and D. Walker. The φ-calculus: a Theory of Mobile Processes. Cambridge University Press, 2001.

Digital Library

[26]

P. Selinger. Towards a quantum programming language. Mathematical Structures in Computer Science, 14(4):527--586, 2004.

Digital Library

[27]

K. Takeuchi, K. Honda, and M. Kubo. An interaction-based language and its typing system. In C. Halatsis, D. G. Maritsas, G. Philokyprou, and S. Theodoridis, editors, PARLE '94: Parallel Architectures and Languages Europe, 6th International PARLE Conference, Proceedings, volume 817 of Lecture Notes in Computer Science. Springer-Verlag, 1994.

Digital Library

[28]

B. Valiron. Quantum typing. In P. Selinger, editor, Proceedings of the Second International Workshop on Quantum Programming Languages, 2004.

[29]

A. van Tonder. A lambda calculus for quantum computation. SIAM Journal on Computing, 33(5):1109--1135, 2004.

Digital Library

[30]

A. K. Wright and M. Felleisen. A syntactic approach to type soundness. Information and Computation, 115(1):38--94, 1994.

Digital Library

Cited By

Jiménez-Pastor ALarsen KTribastone MTschaikowski M(2024)Forward and Backward Constrained Bisimulations for Quantum CircuitsTools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-031-57249-4_17(343-362)Online publication date: 5-Apr-2024
https://doi.org/10.1007/978-3-031-57249-4_17
Lewis MSoudjani SZuliani P(2023)Formal Verification of Quantum Programs: Theory, Tools, and ChallengesACM Transactions on Quantum Computing10.1145/36244835:1(1-35)Online publication date: 16-Dec-2023
https://dl.acm.org/doi/10.1145/3624483
Jamal MAhmad Zafar NAtta-ur-Rahman Musleh DA. Gollapalli MChabani S(2022)Modeling and Verification of Aircraft Takeoff Through Novel Quantum NetsComputers, Materials & Continua10.32604/cmc.2022.02520572:2(3331-3348)Online publication date: 2022
https://doi.org/10.32604/cmc.2022.025205
Show More Cited By

Index Terms

Communicating quantum processes
1. Software and its engineering
  1. Software notations and tools
    1. Formal language definitions
2. Theory of computation
  1. Formal languages and automata theory
  2. Semantics and reasoning
    1. Program reasoning
      1. Program specifications
    2. Program semantics
      1. Operational semantics

Recommendations

Communicating quantum processes
POPL '05: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages

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 ...
Distributed Measurement-based Quantum Computation

We develop a formal model for distributed measurement-based quantum computations, adopting an agent-based view, such that computations are described locally where possible. Because the network quantum state is in general entangled, we need to model it ...
Can quantum discord increase in a quantum communication task?

Quantum teleportation of an unknown quantum state is one of the few communication tasks which has no classical counterpart. Usually the aim of teleportation is to send an unknown quantum state to a receiver. But is it possible in some way that the ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 40, Issue 1

Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages

January 2005

391 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/1047659

Issue’s Table of Contents

POPL '05: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages
January 2005
402 pages
ISBN:158113830X
DOI:10.1145/1040305
General Chair:
Jens Palsberg
University of California, Los Angeles, CA
,
Program Chair:
Martín Abadi
University of California, Santa Cruz, CA

Copyright © 2005 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 12 January 2005

Published in SIGPLAN Volume 40, Issue 1

Check for updates

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

70
Total Citations
View Citations
961
Total Downloads

Downloads (Last 12 months)28
Downloads (Last 6 weeks)5

Reflects downloads up to 21 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Jiménez-Pastor ALarsen KTribastone MTschaikowski M(2024)Forward and Backward Constrained Bisimulations for Quantum CircuitsTools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-031-57249-4_17(343-362)Online publication date: 5-Apr-2024
https://doi.org/10.1007/978-3-031-57249-4_17
Lewis MSoudjani SZuliani P(2023)Formal Verification of Quantum Programs: Theory, Tools, and ChallengesACM Transactions on Quantum Computing10.1145/36244835:1(1-35)Online publication date: 16-Dec-2023
https://dl.acm.org/doi/10.1145/3624483
Jamal MAhmad Zafar NAtta-ur-Rahman Musleh DA. Gollapalli MChabani S(2022)Modeling and Verification of Aircraft Takeoff Through Novel Quantum NetsComputers, Materials & Continua10.32604/cmc.2022.02520572:2(3331-3348)Online publication date: 2022
https://doi.org/10.32604/cmc.2022.025205
Liu ASun M(2019)A Coalgebraic Semantics Framework for Quantum SystemsFormal Methods and Software Engineering10.1007/978-3-030-32409-4_24(387-402)Online publication date: 28-Oct-2019
https://doi.org/10.1007/978-3-030-32409-4_24
Dal Lago URioli A(2015)Applicative Bisimulation and Quantum λ-CalculiFundamentals of Software Engineering10.1007/978-3-319-24644-4_4(54-68)Online publication date: 12-Nov-2015
https://doi.org/10.1007/978-3-319-24644-4_4
Gay SPuthoor I(2015)Equational Reasoning About Quantum ProtocolsReversible Computation10.1007/978-3-319-20860-2_10(155-170)Online publication date: 20-Jun-2015
https://doi.org/10.1007/978-3-319-20860-2_10
Ardeshir-Larijani EGay SNagarajan R(2014)Verification of Concurrent Quantum Protocols by Equivalence CheckingTools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-642-54862-8_42(500-514)Online publication date: 2014
https://doi.org/10.1007/978-3-642-54862-8_42
Franke-Arnold SGay SPuthoor I(2013)Quantum process calculus for linear optical quantum computingProceedings of the 5th international conference on Reversible Computation10.1007/978-3-642-38986-3_19(234-246)Online publication date: 4-Jul-2013
https://dl.acm.org/doi/10.1007/978-3-642-38986-3_19
Ardeshir-Larijani EGay SNagarajan R(2013)Equivalence checking of quantum protocolsProceedings of the 19th international conference on Tools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-642-36742-7_33(478-492)Online publication date: 16-Mar-2013
https://dl.acm.org/doi/10.1007/978-3-642-36742-7_33
Deng YFeng Y(2012)Open bisimulation for quantum processesProceedings of the 7th IFIP TC 1/WG 202 international conference on Theoretical Computer Science10.1007/978-3-642-33475-7_9(119-133)Online publication date: 26-Sep-2012
https://dl.acm.org/doi/10.1007/978-3-642-33475-7_9
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents