More Web Proxy on the site http://driver.im/

Article

Communicating quantum processes

Authors:

Rajagopal NagarajanAuthors Info & Claims

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

Pages 145 - 157

https://doi.org/10.1145/1040305.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

Ceragioli LGadducci FLomurno GTedeschi G(2024)Quantum Bisimilarity via Barbs and Contexts: Curbing the Power of Non-deterministic ObserversProceedings of the ACM on Programming Languages10.1145/36328858:POPL(1269-1297)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632885
Ferreira FCampos J(2024)An Exploratory Study on the Usage of Quantum Programming LanguagesScience of Computer Programming10.1016/j.scico.2024.103217(103217)Online publication date: Oct-2024
https://doi.org/10.1016/j.scico.2024.103217
Wu HYang QLong H(2024)Branching bisimulation semantics for quantum processesInformation Processing Letters10.1016/j.ipl.2024.106492186:COnline publication date: 1-Aug-2024
https://dl.acm.org/doi/10.1016/j.ipl.2024.106492
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

Bisimulation for Quantum Processes

Quantum cryptographic systems have been commercially available, with a striking advantage over classical systems that their security and ability to detect the presence of eavesdropping are provable based on the principles of quantum mechanics. On the ...
Communicating quantum processes
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 ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

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

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

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]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 12 January 2005

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

POPL05

Sponsor:

POPL05: The 32nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages 2005

January 12 - 14, 2005

California, Long Beach, USA

Acceptance Rates

Overall Acceptance Rate 824 of 4,130 submissions, 20%

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

71
Total Citations
View Citations
964
Total Downloads

Downloads (Last 12 months)29
Downloads (Last 6 weeks)2

Reflects downloads up to 12 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Ceragioli LGadducci FLomurno GTedeschi G(2024)Quantum Bisimilarity via Barbs and Contexts: Curbing the Power of Non-deterministic ObserversProceedings of the ACM on Programming Languages10.1145/36328858:POPL(1269-1297)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632885
Ferreira FCampos J(2024)An Exploratory Study on the Usage of Quantum Programming LanguagesScience of Computer Programming10.1016/j.scico.2024.103217(103217)Online publication date: Oct-2024
https://doi.org/10.1016/j.scico.2024.103217
Wu HYang QLong H(2024)Branching bisimulation semantics for quantum processesInformation Processing Letters10.1016/j.ipl.2024.106492186:COnline publication date: 1-Aug-2024
https://dl.acm.org/doi/10.1016/j.ipl.2024.106492
Ceragioli LGadducci FLomurno GTedeschi G(2024)Quantum Bisimilarity Is a Congruence Under Physically Admissible SchedulersProgramming Languages and Systems10.1007/978-981-97-8943-6_9(176-195)Online publication date: 28-Oct-2024
https://doi.org/10.1007/978-981-97-8943-6_9
Lanese IDal Lago UChoudhury V(2024)Towards Quantum Multiparty Session TypesSoftware Engineering and Formal Methods10.1007/978-3-031-77382-2_22(385-403)Online publication date: 4-Nov-2024
https://dl.acm.org/doi/10.1007/978-3-031-77382-2_22
Ceragioli LGadducci FLomurno GTedeschi G(2024)Testing Quantum ProcessesLeveraging Applications of Formal Methods, Verification and Validation. REoCAS Colloquium in Honor of Rocco De Nicola10.1007/978-3-031-73709-1_9(132-151)Online publication date: 9-Oct-2024
https://doi.org/10.1007/978-3-031-73709-1_9
Mousavi MPeters KSchmitt A(2024)Towards a Formal Testing Theory for Quantum ProcessesLeveraging Applications of Formal Methods, Verification and Validation. REoCAS Colloquium in Honor of Rocco De Nicola10.1007/978-3-031-73709-1_8(111-131)Online publication date: 27-Oct-2024
https://dl.acm.org/doi/10.1007/978-3-031-73709-1_8
Arrighi PCedzich CCostes MRémond UValiron B(2023)Addressable Quantum GatesACM Transactions on Quantum Computing10.1145/35817604:3(1-41)Online publication date: 24-Apr-2023
https://dl.acm.org/doi/10.1145/3581760
Bornat RNagarajan R(2023)Describing and Animating Quantum ProtocolsSamson Abramsky on Logic and Structure in Computer Science and Beyond10.1007/978-3-031-24117-8_12(447-473)Online publication date: 2-Aug-2023
https://doi.org/10.1007/978-3-031-24117-8_12
Serrano MCruz-Lemus JPerez-Castillo RPiattini M(2022)Quantum Software Components and Platforms: Overview and Quality AssessmentACM Computing Surveys10.1145/354867955:8(1-31)Online publication date: 23-Dec-2022
https://dl.acm.org/doi/10.1145/3548679
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 Table of Contents