×

Describing and animating quantum protocols. (English) Zbl 07920685

Palmigiano, Alessandra (ed.) et al., Samson Abramsky on logic and structure in computer science and beyond. Cham: Springer. Outst. Contrib. Log. 25, 447-473 (2023).
Summary: We introduce a quantum protocol simulator, the Qtpi simulator, which allows description of quantum protocols with multiple agents. It has protection against cloning and sharing of qbits within a simulation. Its symbolic calculator is adequate for the protocols we have examined, and can be pushed to simulate some non-protocol algorithms.
For the entire collection see [Zbl 1543.68015].

MSC:

03B70 Logic in computer science
68Qxx Theory of computing
81P68 Quantum computation

Software:

QPL; Miranda
Full Text: DOI

References:

[1] Abramsky, S., & Bornat, R. (1983). Pascal-m: a language for loosely-coupled distributed systems. In Y. Paker & J.P. Verjus (Eds.), Distributed Computing Systems (Synchronisation, Control and Communication) (pp. 163-189). Academic Press.
[2] Bennett, C. H., & Brassard, G. (1984). Quantum cryptography: Public key distribution and coin tossing. In Proceedings of IEEE International Conference on Computers, Systems, and Signal Processing, India (p. 175). · Zbl 1306.81030
[3] Bennett, C. H., Brassard, G., Crépeau, C., Jozsa, R., Peres, A., & Wootters, W. K. (1993). Teleporting an unknown quantum state via dual classical and Einstein-Podolsky-Rosen channels. Physical Review Letters, 70(13). · Zbl 1051.81505
[4] Boender, J.; Kammüller, F.; Nagarajan, R., Formalization of quantum protocols using Coq, EPTCS, 195, 71-83 (2015) · Zbl 1477.68528 · doi:10.4204/EPTCS.195.6
[5] Bornat, R. (1986). A protocol for generalized occam. Software: Practice & Experience, 16(9), 783-799. · Zbl 0599.68032
[6] Chen, L., Jordan, S., Liu, Y.-K., Moody, D., Peralta, R., Perlner, R., & Smith-Tone, D. (2016). Report on post-quantum cryptography (Vol. 12). US Department of Commerce, National Institute of Standards and Technology.
[7] Dür, W., Vidal, G., & Cirac, J. I. (2000). Three qubits can be entangled in two inequivalent ways. Physical Review A, 62(6), 062314.
[8] Ekert, A. K., Rarity, J. G., Tapster, P. R., & Palma, G. M. (1992). Practical quantum cryptography based on two-photon interferometry. Phys. Rev. Lett., 69, 1293-1295. DOI: doi:10.1103/PhysRevLett.69.1293.
[9] Ferracin, S.; Kapourniotis, T.; Datta, A., Reducing resources for verification of quantum computations, Physical Review A, 98, 2 (2018) · doi:10.1103/PhysRevA.98.022323
[10] Gay, S. J., & Nagarajan, R. (2005). Communicating quantum processes. In 32nd Symposium on Principles of Programming Languages (POPL 2005) (pp. 145-157). doi:10.1145/1040305.1040318. Also arXiv:quant-ph/0409052. · Zbl 1369.68207
[11] Grover, L. K. (1996). A fast quantum mechanical algorithm for database search. In Proceedings of the Twenty-Eighth Annual ACM Symposium on Theory of Computing (pp. 212-219). · Zbl 0922.68044
[12] Kobayashi, N., Pierce, B. C., & Turner, D. N. (1999). Linearity and the pi-calculus. ACM Transactions on Programming Languages and Systems (TOPLAS), 21(5), 914-947.
[13] Kocher, P., Horn, J., Fogh, A., Genkin, D., Gruss, D., Haas, W., Hamburg, M., Lipp, M., Mangard, S., Prescher, T. et al. (2019). Spectre attacks: Exploiting speculative execution. In 2019 IEEE Symposium on Security and Privacy (SP) (pp. 1-19). IEEE.
[14] Meyer, D. A. (1999). Quantum strategies. Physical Review Letters, 82(5), 1052. · Zbl 0958.81007
[15] Microsoft. Q# kata on superposition, task 16, WState_PowerOfTwo_Reference, Aug 2020. Retrieved October 08, 2020, from https://github.com/microsoft/QuantumKatas/tree/main/Superposition/ReferenceImplementation.qs.
[16] Milner, R., A theory of type polymorphism in programming, Journal of Computer and System Sciences, 17, 3, 348-375 (1978) · Zbl 0388.68003 · doi:10.1016/0022-0000(78)90014-4
[17] Milner, R.; Parrow, J.; Walker, D., A calculus of mobile processes, i, Information and Computation, 100, 1, 1-40 (1992) · Zbl 0752.68036 · doi:10.1016/0890-5401(92)90008-4
[18] Milner, R., Tofte, M., Harper, R., & MacQueen, D. ( 1997). The definition of standard ML: revised. MIT Press.
[19] Ocaml. https://www.ocaml.org.
[20] O’Hearn, P., Reynolds, J. C., & Yang, H. (2001). Local reasoning about programs that alter data structures. In L. Fribourg (Ed.), CSL 2001 (pp. 1-19). Springer. LNCS 2142. · Zbl 0999.68045
[21] Qtpi quantum simulator. https://www.github.com/mdxtoc/qtpi.
[22] Rieffel, EG; Polak, W., An introduction to quantum computing for non-physicists, ACM Computing Surveys, 32, 3, 300-335 (2000) · doi:10.1145/367701.367709
[23] Selinger, P., Towards a quantum programming language, Mathematical Structures in Computer Science, 14, 4, 527-586 (2004) · Zbl 1085.68014 · doi:10.1017/S0960129504004256
[24] Shor, P. W. (1994). Algorithms for quantum computation: Discrete logarithms and factoring. In FOCS (pp. 124-134). IEEE Computer Society.
[25] Status Report on the Second Round of the NIST Post-Quantum Cryptography Standardization Process, July 2020. Retrieved October 10, 2020, from https://csrc.nist.gov/publications/detail/nistir/8309/final.
[26] The Q# Programming Language. https://www.docs.microsoft.com/en-us/quantum/quantum-qr-intro.
[27] Turner, D. A. (1989). Miranda system manual. Retrieved from October 08, 2020, from https://www.cs.kent.ac.uk/people/staff/dat/miranda/manual/.
[28] Turner, D. A. (1985). Miranda: A non-strict functional language with polymorphic types. In Proceedings of a Conference on Functional Programming Languages and Computer Architecture, New York, NY, USA (pp. 1-16). New York: Springer. ISBN 3-387-15975-4. · Zbl 0592.68014
[29] Wegman, M. N., & Carter, J. L. (1981). New hash functions and their use in authentication and set equality. Journal of Computer and System Sciences, 22(3), 265-279. · Zbl 0461.68074
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.