{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,3]],"date-time":"2026-02-03T20:49:53Z","timestamp":1770151793985,"version":"3.49.0"},"reference-count":44,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T00:00:00Z","timestamp":1576800000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2020,1]]},"abstract":"<jats:p>Relational verification of quantum programs has many potential applications in quantum and post-quantum security and other domains. We propose a relational program logic for quantum programs. The interpretation of our logic is based on a quantum analogue of probabilistic couplings. We use our logic to verify non-trivial relational properties of quantum programs, including uniformity for samples generated by the quantum Bernoulli factory, reliability of quantum teleportation against noise (bit and phase flip), security of quantum one-time pad and equivalence of quantum walks.<\/jats:p>","DOI":"10.1145\/3371089","type":"journal-article","created":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T19:45:25Z","timestamp":1576871125000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":28,"title":["Relational proofs for quantum programs"],"prefix":"10.1145","volume":"4","author":[{"given":"Gilles","family":"Barthe","sequence":"first","affiliation":[{"name":"MPI for Security and Privacy, Germany \/ IMDEA Software Institute, Spain"}]},{"given":"Justin","family":"Hsu","sequence":"additional","affiliation":[{"name":"University of Wisconsin-Madison, USA"}]},{"given":"Mingsheng","family":"Ying","sequence":"additional","affiliation":[{"name":"University of Technology Sydney, Australia \/ Institute of Software at Chinese Academy of Sciences, China \/ Tsinghua University, China"}]},{"given":"Nengkun","family":"Yu","sequence":"additional","affiliation":[{"name":"University of Technology Sydney, Australia"}]},{"given":"Li","family":"Zhou","sequence":"additional","affiliation":[{"name":"MPI for Security and Privacy, Germany \/ Tsinghua University, China"}]}],"member":"320","published-online":{"date-parts":[[2019,12,20]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3313276.3316378"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2004.1319636"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1002\/1098-2418(200101)18:1&#38;lt;1::AID-RSA1&#38;gt;3.0.CO;2-7"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_33"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-48899-7_27"},{"key":"e_1_2_2_6_1","volume-title":"21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun, Botswana, 7-12th","volume":"46","author":"Barthe Gilles","year":"2017","unstructured":"Gilles Barthe , Thomas Espitau , Benjamin Gr\u00e9goire , Justin Hsu , and Pierre-Yves Strub . 2017 . Proving uniformity and independence by self-composition and coupling. In LPAR-21 , 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun, Botswana, 7-12th May 2017 (EPiC Series), Thomas Eiter and David Sands (Eds.) , Vol. 46 . EasyChair, 385\u2013403. http:\/\/www.easychair.org\/publications\/paper\/340344 Gilles Barthe, Thomas Espitau, Benjamin Gr\u00e9goire, Justin Hsu, and Pierre-Yves Strub. 2017. Proving uniformity and independence by self-composition and coupling. In LPAR-21, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun, Botswana, 7-12th May 2017 (EPiC Series), Thomas Eiter and David Sands (Eds.), Vol. 46. EasyChair, 385\u2013403. http:\/\/www.easychair.org\/publications\/paper\/340344"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158145"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2934554"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480894"},{"key":"e_1_2_2_10_1","volume-title":"Relational Proofs for Quantum Programs (Extended Version). CoRR abs\/1901.05184","author":"Barthe Gilles","year":"2019","unstructured":"Gilles Barthe , Justin Hsu , Mingsheng Ying , Nengkun Yu , and Li Zhou . 2019. Relational Proofs for Quantum Programs (Extended Version). CoRR abs\/1901.05184 ( 2019 ). arXiv: 1901.05184 http:\/\/arxiv.org\/abs\/1901.05184 Gilles Barthe, Justin Hsu, Mingsheng Ying, Nengkun Yu, and Li Zhou. 2019. Relational Proofs for Quantum Programs (Extended Version). CoRR abs\/1901.05184 (2019). arXiv: 1901.05184 http:\/\/arxiv.org\/abs\/1901.05184"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103670"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2492061"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevLett.70.1895"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.67.042317"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.04.003"},{"key":"e_1_2_2_16_1","volume-title":"Provable quantum advantage in randomness processing. Nature communications 6","author":"Dale Howard","year":"2015","unstructured":"Howard Dale , David Jennings , and Terry Rudolph . 2015. Provable quantum advantage in randomness processing. Nature communications 6 ( 2015 ), 8203. Howard Dale, David Jennings, and Terry Rudolph. 2015. Provable quantum advantage in randomness processing. Nature communications 6 (2015), 8203."},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129506005251"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2007.06.011"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2015.441"},{"key":"e_1_2_2_20_1","volume-title":"Probabilistic Couplings for Probabilistic Reasoning. CoRR abs\/1710.09951","author":"Hsu Justin","year":"2017","unstructured":"Justin Hsu . 2017. Probabilistic Couplings for Probabilistic Reasoning. CoRR abs\/1710.09951 ( 2017 ). arXiv: 1710.09951 http:\/\/arxiv.org\/abs\/1710.09951 Justin Hsu. 2017. Probabilistic Couplings for Probabilistic Reasoning. CoRR abs\/1710.09951 (2017). arXiv: 1710.09951 http:\/\/arxiv.org\/abs\/1710.09951"},{"key":"e_1_2_2_21_1","volume-title":"Quantitative Robustness Analysis of Quantum Programs (Extended Version). CoRR abs\/1811.03585","author":"Hung Shih-Han","year":"2018","unstructured":"Shih-Han Hung , Kesha Hietala , Shaopeng Zhu , Mingsheng Ying , Michael Hicks , and Xiaodi Wu. 2018. Quantitative Robustness Analysis of Quantum Programs (Extended Version). CoRR abs\/1811.03585 ( 2018 ). arXiv: 1811.03585 http: \/\/arxiv.org\/abs\/1811.03585 To appear at POPL\u2019 19. Shih-Han Hung, Kesha Hietala, Shaopeng Zhu, Mingsheng Ying, Michael Hicks, and Xiaodi Wu. 2018. Quantitative Robustness Analysis of Quantum Programs (Extended Version). CoRR abs\/1811.03585 (2018). arXiv: 1811.03585 http: \/\/arxiv.org\/abs\/1811.03585 To appear at POPL\u201919."},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10622-4_7"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/175007.175019"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1080\/00107151031000110776"},{"key":"e_1_2_2_25_1","volume-title":"Automated Verification of Equivalence on Quantum Cryptographic Protocols. In 5th International Symposium on Symbolic Computation in Software Science, SCSS","volume":"15","author":"Kubota Takahiro","year":"2013","unstructured":"Takahiro Kubota , Yoshihiko Kakutani , Go Kato , Yasuhito Kawano , and Hideki Sakurada . 2013 . Automated Verification of Equivalence on Quantum Cryptographic Protocols. In 5th International Symposium on Symbolic Computation in Software Science, SCSS 2013, Castle of Hagenberg, Austria (EPiC Series in Computing), Laura Kov\u00e1cs and Temur Kutsia (Eds.) , Vol. 15 . EasyChair, 64\u201369. http:\/\/www.easychair.org\/publications\/paper\/143661 Takahiro Kubota, Yoshihiko Kakutani, Go Kato, Yasuhito Kawano, and Hideki Sakurada. 2013. Automated Verification of Equivalence on Quantum Cryptographic Protocols. In 5th International Symposium on Symbolic Computation in Software Science, SCSS 2013, Castle of Hagenberg, Austria (EPiC Series in Computing), Laura Kov\u00e1cs and Temur Kutsia (Eds.), Vol. 15. EasyChair, 64\u201369. http:\/\/www.easychair.org\/publications\/paper\/143661"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0219025716500120"},{"key":"e_1_2_2_27_1","volume-title":"Quantum Relational Hoare Logic with Expectations. CoRR abs\/1903.08357","author":"Li Yangjia","year":"2019","unstructured":"Yangjia Li and Dominique Unruh . 2019. Quantum Relational Hoare Logic with Expectations. CoRR abs\/1903.08357 ( 2019 ). arXiv: 1903.08357 http:\/\/arxiv.org\/abs\/1903.08357 Yangjia Li and Dominique Unruh. 2019. Quantum Relational Hoare Logic with Expectations. CoRR abs\/1903.08357 (2019). arXiv: 1903.08357 http:\/\/arxiv.org\/abs\/1903.08357"},{"key":"e_1_2_2_28_1","volume-title":"Lectures on the coupling method","author":"Lindvall Torgny","unstructured":"Torgny Lindvall . 2002. Lectures on the coupling method . Courier Corporation . Torgny Lindvall. 2002. Lectures on the coupling method. Courier Corporation."},{"key":"e_1_2_2_29_1","volume-title":"Private quantum channels and the cost of randomizing quantum information. arXiv preprint quant-ph\/0003101","author":"Mosca Michele","year":"2000","unstructured":"Michele Mosca , Alain Tapp , and Ronald de Wolf . 2000. Private quantum channels and the cost of randomizing quantum information. arXiv preprint quant-ph\/0003101 ( 2000 ). https:\/\/arxiv.org\/abs\/quant- ph\/0003101 Michele Mosca, Alain Tapp, and Ronald de Wolf. 2000. Private quantum channels and the cost of randomizing quantum information. arXiv preprint quant-ph\/0003101 (2000). https:\/\/arxiv.org\/abs\/quant- ph\/0003101"},{"key":"e_1_2_2_30_1","volume-title":"Quantum computation and quantum information","author":"Nielsen Michael A","unstructured":"Michael A Nielsen and Isaac Chuang . 2002. Quantum computation and quantum information . Cambridge University Press . Michael A Nielsen and Isaac Chuang. 2002. Quantum computation and quantum information. Cambridge University Press."},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24754-8_1"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129504004256"},{"key":"e_1_2_2_33_1","volume-title":"The existence of probability measures with given marginals. The Annals of Mathematical Statistics","author":"Strassen Volker","year":"1965","unstructured":"Volker Strassen . 1965. The existence of probability measures with given marginals. The Annals of Mathematical Statistics ( 1965 ), 423\u2013439. http:\/\/projecteuclid.org\/euclid.aoms\/1177700153 Volker Strassen. 1965. The existence of probability measures with given marginals. The Annals of Mathematical Statistics (1965), 423\u2013439. http:\/\/projecteuclid.org\/euclid.aoms\/1177700153"},{"key":"e_1_2_2_34_1","doi-asserted-by":"crossref","unstructured":"Hermann Thorisson. 2000. Coupling Stationarity and Regeneration. springer.  Hermann Thorisson. 2000. Coupling Stationarity and Regeneration. springer.","DOI":"10.1007\/978-1-4612-1236-2"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2019.8785779"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290346"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11128-012-0432-5"},{"key":"e_1_2_2_38_1","doi-asserted-by":"crossref","unstructured":"C\u00e9dric Villani. 2008. Optimal transport: Old and new. springer.  C\u00e9dric Villani. 2008. Optimal transport: Old and new. springer.","DOI":"10.1007\/978-3-540-71050-9"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00220-016-2609-8"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2049706.2049708"},{"key":"e_1_2_2_41_1","doi-asserted-by":"crossref","unstructured":"Mingsheng Ying. 2016. Foundations of Quantum Programming. Morgan-Kaufmann.  Mingsheng Ying. 2016. Foundations of Quantum Programming. Morgan-Kaufmann.","DOI":"10.1016\/B978-0-12-802306-8.00004-5"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2013.03.016"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2019.08.026"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314584"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3371089","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3371089","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T19:05:43Z","timestamp":1750273543000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3371089"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,12,20]]},"references-count":44,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2020,1]]}},"alternative-id":["10.1145\/3371089"],"URL":"https:\/\/doi.org\/10.1145\/3371089","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,12,20]]},"assertion":[{"value":"2019-12-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}