×

Certified quantum computation in Isabelle/HOL. (English) Zbl 07432184

Summary: In this article we present an ongoing effort to formalise quantum algorithms and results in quantum information theory using the proof assistant Isabelle/HOL. Formal methods being critical for the safety and security of algorithms and protocols, we foresee their widespread use for quantum computing in the future. We have developed a large library for quantum computing in Isabelle based on a matrix representation for quantum circuits, successfully formalising the no-cloning theorem, quantum teleportation, Deutsch’s algorithm, the Deutsch-Jozsa algorithm and the quantum Prisoner’s Dilemma. We discuss the design choices made and report on an outcome of our work in the field of quantum game theory.

MSC:

03B35 Mechanization of proofs and logical operations
03B15 Higher-order logic; type theory (MSC2010)
81P68 Quantum computation
68Q12 Quantum algorithms and complexity in the theory of computing
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] Liu, J.; Zhan, B.; Wang, S.; Ying, S.; Liu, T.; Li, Y.; Ying, M.; Zhan, N.; Dillig, I.; Tasiran, S., Formal verification of quantum algorithms using quantum hoare logic, Computer Aided Verification, 187-207 (2019), Cham: Springer, Cham · doi:10.1007/978-3-030-25543-5_12
[2] Rand, R.; Paykin, J.; Zdancewic, S., QWIRE practice: formal verification of quantum circuits in coq, EPTCS, 266, 119-132 (2018) · Zbl 1486.81065 · doi:10.4204/EPTCS.266.8
[3] Boender, J., Kammüller, F., Nagarajan, R.: Formalization of Quantum Protocols using Coq. In: QPL (2015)
[4] Ballarin, C., Locales: a module system for mathematical theories, J. Autom. Reason., 52, 2, 123-153 (2014) · Zbl 1315.68218 · doi:10.1007/s10817-013-9284-7
[5] Thiemann, R., Yamada, A.: Matrices, Jordan normal forms, and spectral radius theory. Archive of Formal Proofs (2015). http://isa-afp.org/entries/Jordan_Normal_Form.html, Formal proof development
[6] Prathamesh, T.V.H.: Tensor product of matrices. Archive of Formal Proofs (2016). http://isa-afp.org/entries/Matrix_Tensor.html, Formal proof development
[7] Nielsen, MA; Chuang, IL, Quantum Computation and Quantum Information: 10th Anniversary Edition (2011), New York: Cambridge University Press, New York · Zbl 1288.81001
[8] Wootters, WK; Zurek, WH, A single quantum cannot be cloned, Nature, 299, 802-803 (1982) · Zbl 1369.81022 · doi:10.1038/299802a0
[9] Dieks, D., Communication by EPR devices, Phys. Lett. A, 92, 271-272 (1982) · doi:10.1016/0375-9601(82)90084-6
[10] Bennett, CH; Brassard, G.; Crépeau, C.; Jozsa, R.; Peres, A.; Wootters, WK, Teleporting an unknown quantum state via dual classical and Einstein-Podolsky-Rosen channels, Phys. Rev. Lett., 70, 1895-1899 (1993) · Zbl 1051.81505 · doi:10.1103/PhysRevLett.70.1895
[11] Deutsch, D., Quantum theory, the Church-Turing principle and the universal quantum computer, Proc. R. Soc. Lond. A, 400, 97-117 (1985) · Zbl 0900.81019 · doi:10.1098/rspa.1985.0070
[12] Osborne, MJ; Rubinstein, A., A Course in Game Theory (1994), Cambridge: MIT Press, Cambridge · Zbl 1194.91003
[13] Eisert, J.; Wilkens, M.; Lewenstein, M., Quantum games and quantum strategies, Phys. Rev. Lett., 83, 3077-3080 (1999) · Zbl 0946.81018 · doi:10.1103/PhysRevLett.83.3077
[14] Benjamin, SC; Hayden, PM, Comment on quantum games and quantum strategies, Phys. Rev. Lett., 87, 069801 (2001) · doi:10.1103/PhysRevLett.87.069801
[15] Flitney, AP; Abbott, D., An introduction to quantum game theory, Fluct. Noise Lett., 02, 4, R175-R187 (2002) · doi:10.1142/S0219477502000981
[16] Eisert, J., Wilkens, M., Lewenstein, M.: Erratum: quantum games and quantum strategies [Phys. Rev. Lett. 83, 3077 (1999)]. Phys. Rev. Lett., 124, 139901 (2020) · Zbl 0946.81018
[17] Paulson, LC, The inductive approach to verifying cryptographic protocols, J. Comput. Secur., 6, 1-2, 85-128 (1998) · doi:10.3233/JCS-1998-61-205
[18] Kammüller, F., Attack trees in Isabelle extended with probabilities for quantum cryptography, Comput. Secur., 87, 101572 (2019) · doi:10.1016/j.cose.2019.101572
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.