{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:09:36Z","timestamp":1776305376806,"version":"3.50.1"},"publisher-location":"Cham","reference-count":71,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030720186","type":"print"},{"value":"9783030720193","type":"electronic"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,3,23]],"date-time":"2021-03-23T00:00:00Z","timestamp":1616457600000},"content-version":"vor","delay-in-days":81,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>While recent progress in quantum hardware open the door for significant speedup in certain key areas, quantum algorithms are still hard to implement right, and the validation of such quantum programs is a challenge. In this paper we propose <jats:sc>Qbricks<\/jats:sc>, a formal verification environment for circuit-building quantum programs, featuring both parametric specifications <jats:italic>and<\/jats:italic> a high degree of proof automation. We propose a logical framework based on first-order logic, and develop the main tool we rely upon for achieving the automation of proofs of quantum specification: PPS, a parametric extension of the recently developed path sum semantics. To back-up our claims, we implement and verify parametric versions of several famous and non-trivial quantum algorithms, including the quantum parts of <jats:italic>Shor\u2019s integer factoring<\/jats:italic>, quantum phase estimation (QPE) and Grover\u2019s search.<\/jats:p>","DOI":"10.1007\/978-3-030-72019-3_6","type":"book-chapter","created":{"date-parts":[[2021,3,22]],"date-time":"2021-03-22T14:03:10Z","timestamp":1616421790000},"page":"148-177","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":46,"title":["An Automated Deductive Verification Framework for Circuit-building Quantum Programs"],"prefix":"10.1007","author":[{"given":"Christophe","family":"Chareton","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"S\u00e9bastien","family":"Bardin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fran\u00e7ois","family":"Bobot","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Valentin","family":"Perrelle","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Beno\u00eet","family":"Valiron","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,3,23]]},"reference":[{"key":"6_CR1","unstructured":"M.\u00a0Amy. Formal Methods in Quantum Circuit Design. PhD thesis, University of Waterloo, Ontario, Canada, 2019."},{"key":"6_CR2","doi-asserted-by":"crossref","unstructured":"M.\u00a0Amy. Towards large-scale functional verification of universal quantum circuits. In P.\u00a0Selinger and G.\u00a0Chiribella, editors, Proceedings 15th International Conference on Quantum Physics and Logic, QPL 2018, volume 287 of Electronic Proceedings in Theoretical Computer Science, pages 1\u201321, Halifax, Canada, 2019. EPTCS.","DOI":"10.4204\/EPTCS.287.1"},{"key":"6_CR3","doi-asserted-by":"crossref","unstructured":"M.\u00a0Amy, M.\u00a0Roetteler, and K.\u00a0M. Svore. Verified compilation of space-efficient reversible circuits. In R.\u00a0Majumdar and V.\u00a0Kuncak, editors, Proceedings of the 29th International Conference on Computer Aided Verification (CAV 2017), Part II, volume 10427 of Lecture Notes in Computer Science, pages 3\u201321, Heidelberg, Germany, 2017. Springer.","DOI":"10.1007\/978-3-319-63390-9_1"},{"key":"6_CR4","doi-asserted-by":"crossref","unstructured":"F.\u00a0Arute, K.\u00a0Arya, R.\u00a0Babbush, D.\u00a0Bacon, J.\u00a0C. Bardin, R.\u00a0Barends, R.\u00a0Biswas, S.\u00a0Boixo, F.\u00a0G. S.\u00a0L. Brandao, D.\u00a0A. Buell, et\u00a0al. Quantum supremacy using a programmable superconducting processor. Nature, 574(7779):505\u2013510, 2019.","DOI":"10.1038\/s41586-019-1666-5"},{"key":"6_CR5","doi-asserted-by":"crossref","unstructured":"S.\u00a0Beauregard. Circuit for shor\u2019s algorithm using 2n+ 3 qubits. arXiv preprint quant-ph\/0205095, 2002.","DOI":"10.26421\/QIC3.2-8"},{"key":"6_CR6","doi-asserted-by":"crossref","unstructured":"D.\u00a0Bhattacharjee, M.\u00a0Soeken, S.\u00a0Dutta, A.\u00a0Chattopadhyay, and G.\u00a0D. Micheli. Reversible pebble games for reducing qubits in hierarchical quantum circuit synthesis. In Proceedings of the 49th IEEE International Symposium on Multiple-Valued Logic (ISMVL 2019), pages 102\u2013107, Fredericton, NB, Canada, 2019. IEEE.","DOI":"10.1109\/ISMVL.2019.00026"},{"key":"6_CR7","doi-asserted-by":"crossref","unstructured":"J.\u00a0Biamonte, P.\u00a0Wittek, N.\u00a0Pancotti, P.\u00a0Rebentrost, N.\u00a0Wiebe, and S.\u00a0Lloyd. Quantum machine learning. Nature, 549(7671):195, 2017.","DOI":"10.1038\/nature23474"},{"key":"6_CR8","doi-asserted-by":"crossref","unstructured":"B.\u00a0Bichsel, M.\u00a0Baader, T.\u00a0Gehr, and M.\u00a0T. Vechev. Silq: a high-level quantum language with safe uncomputation and intuitive semantics. In A.\u00a0F. Donaldson and E.\u00a0Torlak, editors, Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2020, London, UK, June 15-20, 2020, pages 286\u2013300. ACM, 2020.","DOI":"10.1145\/3385412.3386007"},{"key":"6_CR9","unstructured":"F.\u00a0Bobot, J.-C. Filli\u00e2tre, C.\u00a0March\u00e9, and A.\u00a0Paskevich. Why3: Shepherd Your Herd of Provers. In Proceedings of Boogie 2011: First International Workshop on Intermediate Verification Languages, Wroclaw, Poland, 53\u201364, 2011. Available online as hal-00790310."},{"key":"6_CR10","doi-asserted-by":"crossref","unstructured":"J. Boender, F. Kamm\u00fcller, and R. Nagarajan. Formalization of quantum protocols using coq. In C. Heunen, P. Selinger, and J. Vicary, editors, Proceedings of the 12th International Workshop on Quantum Physics and Logic (QPL 2015), volume 195 of Electronic Proceedings in Theoretical Computer Science, pages 71\u201383, Oxford, UK, 2015. EPTCS.","DOI":"10.4204\/EPTCS.195.6"},{"key":"6_CR11","doi-asserted-by":"crossref","unstructured":"A.\u00a0Broadbent. How to verify a quantum computation. Theory of Computing, 14(1):1\u201337, 2018.","DOI":"10.4086\/toc.2018.v014a011"},{"key":"6_CR12","unstructured":"T.\u00a0Carette, D.\u00a0Horsman, and S.\u00a0Perdrix. SZX-calculus: Scalable graphical quantum reasoning. In P.\u00a0Rossmanith, P.\u00a0Heggernes, and J.\u00a0Katoen, editors, 44th International Symposium on Mathematical Foundations of Computer Science, MFCS 2019, August 26-30, 2019, Aachen, Germany, volume 138 of LIPIcs, pages 55:1\u201355:15. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 2019."},{"key":"6_CR13","unstructured":"C.\u00a0Chareton, S.\u00a0Bardin, F.\u00a0Bobot, V.\u00a0Perrelle, and B.\u00a0Valiron. Toward certified quantum programming. arXiv preprint\u00a0arXiv:2003.05841, 2020."},{"key":"6_CR14","doi-asserted-by":"crossref","unstructured":"I.\u00a0L. Chuang, N.\u00a0Gershenfeld, and M.\u00a0Kubinec. Experimental implementation of fast quantum searching. Physical review letters, 80(15):3408, 1998.","DOI":"10.1103\/PhysRevLett.80.3408"},{"key":"6_CR15","doi-asserted-by":"crossref","unstructured":"E.\u00a0M. Clarke and J.\u00a0M. Wing. Formal methods: State of the art and future directions. ACM Computing Surveys (CSUR), 28(4):626\u2013643, 1996.","DOI":"10.1145\/242223.242257"},{"key":"6_CR16","doi-asserted-by":"crossref","unstructured":"R.\u00a0Cleve, A.\u00a0Ekert, C.\u00a0Macchiavello, and M.\u00a0Mosca. Quantum algorithms revisited. Proceedings of the Royal Society of London. Series A: Mathematical, Physical and Engineering Sciences, 454(1969):339\u2013354, 1998.","DOI":"10.1098\/rspa.1998.0164"},{"key":"6_CR17","doi-asserted-by":"crossref","unstructured":"B.\u00a0Coecke and A.\u00a0Kissinger. Picturing quantum processes. Cambridge University Press, Cambridge, United Kingdom, 2017.","DOI":"10.1017\/9781316219317"},{"key":"6_CR18","unstructured":"D.\u00a0Coppersmith. An approximate fourier transform useful in quantum factoring. arXiv preprint quant-ph\/0201067, 1994."},{"key":"6_CR19","unstructured":"T.\u00a0A. Davidson. Formal verification techniques using quantum process calculus. PhD thesis, University of Warwick, 2012."},{"key":"6_CR20","doi-asserted-by":"crossref","unstructured":"N.\u00a0de\u00a0Beaudrap, R.\u00a0Duncan, D.\u00a0Horsman, and S.\u00a0Perdrix. Pauli fusion: a computational model to realise quantum transformations from ZX terms. Available online as arXiv:1904.12817, 2019.","DOI":"10.4204\/EPTCS.318.6"},{"key":"6_CR21","doi-asserted-by":"crossref","unstructured":"A.\u00a0Fagan and R.\u00a0Duncan. Optimising Clifford circuits with Quantomatic. In P.\u00a0Selinger and G.\u00a0Chiribella, editors, Proceedings of the 15th International Conference on Quantum Physics and Logic (QPL 2018), volume 287 of Electronic Notes In Theoretical Computer Science, pages 85\u2013105, Halifax, Canada, 2018. EPTCS.","DOI":"10.4204\/EPTCS.287.5"},{"key":"6_CR22","unstructured":"E. Farhi, J. Goldstone, and S. Gutmann. A quantum approximate optimization algorithm. Available online as arXiv:1411.4028, 2014."},{"key":"6_CR23","doi-asserted-by":"crossref","unstructured":"E.\u00a0Farhi, J.\u00a0Goldstone, S.\u00a0Gutmann, J.\u00a0Lapan, A.\u00a0Lundgren, and D.\u00a0Preda. A quantum adiabatic evolution algorithm applied to random instances of an np-complete problem. Science, 292(5516):472\u2013475, 2001.","DOI":"10.1126\/science.1057726"},{"key":"6_CR24","doi-asserted-by":"crossref","unstructured":"J.\u00a0Filli\u00e2tre and C.\u00a0March\u00e9. The Why\/Krakatoa\/Caduceus platform for deductive program verification. In W.\u00a0Damm and H.\u00a0Hermanns, editors, Proceedings of the 19th International Conference on Computer Aided Verification (CAV 2007), volume 4590 of Lecture Notes in Computer Science, pages 173\u2013177, Berlin, Germany, 2007. Springer.","DOI":"10.1007\/978-3-540-73368-3_21"},{"key":"6_CR25","unstructured":"J.\u00a0Filli\u00e2tre and A.\u00a0Paskevich. Why3 - where programs meet provers. In M.\u00a0Felleisen and P.\u00a0Gardner, editors, Proceedings of the 22nd European Symposium on Programming Languages and Systems (ESOP 2013), Held as Part of the European Joint Conferences on Theory and Practice of Software (ETAPS 2013), volume 7792 of Lecture Notes in Computer Science, pages 125\u2013128, Rome, Italy, 2013. Springer."},{"key":"6_CR26","doi-asserted-by":"crossref","unstructured":"J.-C. Filli\u00e2tre, L.\u00a0Gondelman, and A.\u00a0Paskevich. The spirit of ghost code. Formal Methods in System Design, 48(3):152\u2013174, 2016.","DOI":"10.1007\/s10703-016-0243-x"},{"key":"6_CR27","doi-asserted-by":"crossref","unstructured":"S.\u00a0J. Gay, R.\u00a0Nagarajan, and N.\u00a0Papanikolaou. QMC: a model checker for quantum systems. In A.\u00a0Gupta and S.\u00a0Malik, editors, Proceeding of the 20th International Conference on Computer Aided Verification (CAV 2008), volume 5123 of Lecture Notes in Computer Science, pages 543\u2013547, Princeton, NJ, USA, 2008. Springer.","DOI":"10.1007\/978-3-540-70545-1_51"},{"key":"6_CR28","doi-asserted-by":"crossref","unstructured":"I.\u00a0M. Georgescu, S.\u00a0Ashhab, and F.\u00a0Nori. Quantum simulation. Reviews of Modern Physics, 86(1):153, 2014.","DOI":"10.1103\/RevModPhys.86.153"},{"key":"6_CR29","doi-asserted-by":"crossref","unstructured":"A.\u00a0Gheorghiu, T.\u00a0Kapourniotis, and E.\u00a0Kashefi. Verification of quantum computation: An overview of existing approaches. Theory of Computing Systems, 63(4):715\u2013808, 2019.","DOI":"10.1007\/s00224-018-9872-3"},{"key":"6_CR30","doi-asserted-by":"crossref","unstructured":"A.\u00a0S. Green, P.\u00a0L. Lumsdaine, N.\u00a0J. Ross, P.\u00a0Selinger, and B.\u00a0Valiron. Quipper: A scalable quantum programming language. In H.-J. Boehm and C.\u00a0Flanagan, editors, Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, (PLDI\u201913), pages 333\u2013342, Seattle, WA, USA, 2013. ACM.","DOI":"10.1145\/2499370.2462177"},{"key":"6_CR31","doi-asserted-by":"crossref","unstructured":"L.\u00a0K. Grover. A fast quantum mechanical algorithm for database search. In G.\u00a0L. Miller, editor, Proceedings of the Twenty-Eighth Annual ACM Symposium on the Theory of Computing (STOC), pages 212\u2013219, Philadelphia, Pennsylvania, USA, 1996. ACM.","DOI":"10.1145\/237814.237866"},{"key":"6_CR32","doi-asserted-by":"crossref","unstructured":"W.\u00a0Haaswijk, M.\u00a0Soeken, A.\u00a0Mishchenko, and G.\u00a0De Micheli. SAT-based exact synthesis: Encodings, topology families, and parallelism. To apprear in IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, https:\/\/doi,org\/10.1109\/TCAD.2019.2897703, 2019.","DOI":"10.1109\/TCAD.2019.2897703"},{"key":"6_CR33","doi-asserted-by":"crossref","unstructured":"A.\u00a0W. Harrow, A.\u00a0Hassidim, and S.\u00a0Lloyd. Quantum algorithm for linear systems of equations. Physical Review Letters, 103:150502, Oct 2009.","DOI":"10.1103\/PhysRevLett.103.150502"},{"key":"6_CR34","unstructured":"K.\u00a0Hietala, R.\u00a0Rand, S.-H. Hung, L.\u00a0Li, and M.\u00a0Hicks. Proving quantum programs correct. arXiv preprint\u00a0arXiv:2010.01240, 2020."},{"key":"6_CR35","doi-asserted-by":"crossref","unstructured":"K.\u00a0Hietala, R.\u00a0Rand, S.-H. Hung, X.\u00a0Wu, and M.\u00a0Hicks. A verified optimizer for quantum circuits. Proceedings of the ACM on Programming Languages, 5(POPL):1\u201329, 2021.","DOI":"10.1145\/3434318"},{"key":"6_CR36","unstructured":"Y.\u00a0Huang and M.\u00a0Martonosi. QDB: from quantum algorithms towards correct quantum programs. In T.\u00a0Barik, J.\u00a0Sunshine, and S.\u00a0Chasins, editors, Proceedings of the 9th Workshop on Evaluation and Usability of Programming Languages and Tools (PLATEAU@SPLASH 2018), volume\u00a067 of OpenAccess Series in Informatics (OASIcs), pages 4:1\u20134:14, Boston, Massachusetts, USA, 2018. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik."},{"key":"6_CR37","doi-asserted-by":"crossref","unstructured":"Y.\u00a0Huang and M.\u00a0Martonosi. Statistical assertions for validating patterns and finding bugs in quantum programs. In S.\u00a0B. Manne, H.\u00a0C. Hunter, and E.\u00a0R. Altman, editors, Proceedings of the 46th International Symposium on Computer Architecture (ISCA 2019), pages 541\u2013553, Phoenix, AZ, USA, 2019. ACM.","DOI":"10.1145\/3307650.3322213"},{"key":"6_CR38","unstructured":"IBM Blog. On quantum supremacy. Blog Article (https:\/\/www.ibm.com\/blogs\/research\/2019\/10\/on-quantum-supremacy\/), 2019."},{"key":"6_CR39","unstructured":"A. Kissinger and J. van de Wetering. Reducing t-count with the ZX-calculus. Available online as arXiv:1903.10477, 2019."},{"key":"6_CR40","doi-asserted-by":"crossref","unstructured":"A.\u00a0Kissinger and V.\u00a0Zamdzhiev. Quantomatic: A proof assistant for diagrammatic reasoning. In A.\u00a0P. Felty and A.\u00a0Middeldorp, editors, Proceedings for the 25th International Conference on Automated Deduction (CADE-25), volume 9195 of Lecture Notes in Computer Science, pages 326\u2013336, Berlin, Germany, 2015. Springer.","DOI":"10.1007\/978-3-319-21401-6_22"},{"key":"6_CR41","unstructured":"A.\u00a0Y. Kitaev. Quantum measurements and the abelian stabilizer problem. Available online as arXiv:quant-ph\/9511026, 1995."},{"key":"6_CR42","unstructured":"E.\u00a0Knill. Conventions for quantum pseudocode. Technical report, Los Alamos National Lab., NM (United States), 1996."},{"key":"6_CR43","doi-asserted-by":"crossref","unstructured":"U.\u00a0D. Lago, A.\u00a0Masini, and M.\u00a0Zorzi. Quantum implicit computational complexity. Theoretical Computer Science, 411(2):377\u2013409, 2010.","DOI":"10.1016\/j.tcs.2009.07.045"},{"key":"6_CR44","doi-asserted-by":"crossref","unstructured":"G.\u00a0Li, L.\u00a0Zhou, N.\u00a0Yu, Y.\u00a0Ding, M.\u00a0Ying, and Y.\u00a0Xie. Projection-based runtime assertions for testing and debugging quantum programs. Proc. ACM Program. Lang., 4(OOPSLA):150:1\u2013150:29, 2020.","DOI":"10.1145\/3428218"},{"key":"6_CR45","doi-asserted-by":"crossref","unstructured":"J.\u00a0Liu, B.\u00a0Zhan, S.\u00a0Wang, S.\u00a0Ying, T.\u00a0Liu, Y.\u00a0Li, M.\u00a0Ying, and N.\u00a0Zhan. Formal verification of quantum algorithms using quantum hoare logic. In I.\u00a0Dillig and S.\u00a0Tasiran, editors, Computer Aided Verification, pages 187\u2013207, Cham, 2019. Springer International Publishing.","DOI":"10.1007\/978-3-030-25543-5_12"},{"key":"6_CR46","unstructured":"T.\u00a0Liu, Y.\u00a0Li, S.\u00a0Wang, M.\u00a0Ying, and N.\u00a0Zhan. A theorem prover for quantum hoare logic and its applications. Available as arXiv:1601.03835, 2016."},{"key":"6_CR47","doi-asserted-by":"crossref","unstructured":"U.\u00a0Mahadev. Classical verification of quantum computations. In M.\u00a0Thorup, editor, Proceedings of the 59th IEEE Annual Symposium on Foundations of Computer Science (FOCS 2018), pages 259\u2013267, Paris, France, 2018. IEEE Computer Society.","DOI":"10.1109\/FOCS.2018.00033"},{"key":"6_CR48","doi-asserted-by":"crossref","unstructured":"G.\u00a0Meuli, M.\u00a0Soeken, M.\u00a0Roetteler, and T.\u00a0H\u00e4ner. Enabling accuracy-aware quantum compilers using symbolic resource estimation. Proc. ACM Program. Lang., 4(OOPSLA), 2020.","DOI":"10.1145\/3428198"},{"key":"6_CR49","unstructured":"R. Nagarajan and S. Gay. Formal verification of quantum protocols. Available online as arXiv:quant-ph\/0203086, 2002."},{"key":"6_CR50","unstructured":"M.\u00a0A. Nielsen and I.\u00a0Chuang. Quantum computation and quantum information. Cambridge University Press, Cambridge, United Kingdom, 2002."},{"key":"6_CR51","doi-asserted-by":"crossref","unstructured":"L.\u00a0Paolini, M.\u00a0Piccolo, and M.\u00a0Zorzi. qPCF: Higher-order languages and quantum circuits. Journal of Automated Reasoning, 63(4):941\u2013966, Dec 2019.","DOI":"10.1007\/s10817-019-09518-y"},{"key":"6_CR52","doi-asserted-by":"crossref","unstructured":"A.\u00a0Parent, M.\u00a0Roetteler, and K.\u00a0M. Svore. REVS: a tool for space-optimized reversible circuit synthesis. In I.\u00a0Phillips and H.\u00a0Rahaman, editors, Proceedings of the 9th International Conference on Reversible Computation (RC 2017), volume 10301 of Lecture Notes in Computer Science, pages 90\u2013101, Kolkata, India, 2017. Springer.","DOI":"10.1007\/978-3-319-59936-6_7"},{"key":"6_CR53","doi-asserted-by":"crossref","unstructured":"J.\u00a0Paykin, R.\u00a0Rand, and S.\u00a0Zdancewic. QWIRE: a core language for quantum circuits. In G.\u00a0Castagna and A.\u00a0D. Gordon, editors, Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL\u201917), pages 846\u2013858, Paris, France, 2017. ACM.","DOI":"10.1145\/3009837.3009894"},{"key":"6_CR54","unstructured":"Qbricks repository. https:\/\/cchareton.github.io\/Qbricks."},{"key":"6_CR55","unstructured":"Quantum Computing Report. List of tools. Available online (https:\/\/quantumcomputingreport.com\/resources\/tools\/), 2019."},{"key":"6_CR56","unstructured":"R.\u00a0Rand. Formally Verified Quantum Programming. PhD thesis, University of Pennsylvania, 2018."},{"key":"6_CR57","doi-asserted-by":"crossref","unstructured":"R.\u00a0Rand, J.\u00a0Paykin, D.\u00a0Lee, and S.\u00a0Zdancewic. ReQWIRE: Reasoning about reversible quantum circuits. In P.\u00a0Selinger and G.\u00a0Chiribella, editors, Proceedings 15th International Conference on Quantum Physics and Logic (QPL 2018), volume 287 of Electronic Proceedings in Theoretical Computer Science, pages 299\u2013312, Halifax, Canada, 2018. EPTCS.","DOI":"10.4204\/EPTCS.287.17"},{"key":"6_CR58","doi-asserted-by":"crossref","unstructured":"R.\u00a0Rand, J.\u00a0Paykin, and S.\u00a0Zdancewic. QWIRE practice: Formal verification of quantum circuits in coq. In B.\u00a0Coecke and A.\u00a0Kissinger, editors, Proceedings 14th International Conference on Quantum Physics and Logic (QPL 2017), volume 266 of Electronic Proceedings in Theoretical Computer Science, pages 119\u2013132, Nijmegen, The Netherlands, 2017. EPTCS.","DOI":"10.4204\/EPTCS.266.8"},{"key":"6_CR59","unstructured":"N.\u00a0J. Ross. Algebraic and Logical Methods in Quantum Computation. PhD thesis, Dalhousie University, 2015."},{"key":"6_CR60","doi-asserted-by":"crossref","unstructured":"P.\u00a0Selinger and B.\u00a0Valiron. A lambda calculus for quantum computation with classical control. Mathematical Structures in Computer Science, 16:527\u2013552, 2006.","DOI":"10.1017\/S0960129506005238"},{"key":"6_CR61","unstructured":"P. W. Shor. Algorithms for quantum computation: Discrete log and factoring. In Proceedings of the 35th Annual Symposium on Foundations of Computer Science (FOCS\u201994), pages 124\u2013134, Santa Fe, New Mexico, US., 1994. IEEE, IEEE Computer Society Press."},{"key":"6_CR62","doi-asserted-by":"crossref","unstructured":"M.\u00a0Soeken, T.\u00a0H\u00e4ner, and M.\u00a0Roetteler. Programming quantum computers using design automation. Available online as arXiv:1803.01022, 2018.","DOI":"10.23919\/DATE.2018.8341993"},{"key":"6_CR63","doi-asserted-by":"crossref","unstructured":"D.\u00a0S. Steiger, T.\u00a0H\u00e4ner, and M.\u00a0Troyer. ProjectQ: an open source software framework for quantum computing. Quantum, 2:49, Jan. 2018.","DOI":"10.22331\/q-2018-01-31-49"},{"key":"6_CR64","doi-asserted-by":"crossref","unstructured":"K.\u00a0M. Svore, A.\u00a0Geller, M.\u00a0Troyer, J.\u00a0Azariah, C.\u00a0Granade, B.\u00a0Heim, V.\u00a0Kliuchnikov, M.\u00a0Mykhailova, A.\u00a0Paz, and M.\u00a0Roetteler. Q#: Enabling scalable quantum computing and development with a high-level domain-specific language. Available online as arXiv:1803.00652, 2018.","DOI":"10.1145\/3183895.3183901"},{"key":"6_CR65","doi-asserted-by":"crossref","unstructured":"K.\u00a0M. Svore and M.\u00a0Troyer. The quantum future of computation. IEEE Computer, 49(9):21\u2013030, 2016.","DOI":"10.1109\/MC.2016.293"},{"key":"6_CR66","doi-asserted-by":"crossref","unstructured":"B.\u00a0Valiron, N.\u00a0J. Ross, P.\u00a0Selinger, D.\u00a0S. Alexander, and J.\u00a0M. Smith. Programming the quantum future. Communications of the ACM, 58(8):52\u201361, 2015.","DOI":"10.1145\/2699415"},{"key":"6_CR67","unstructured":"D.\u00a0Wecker and K.\u00a0M. Svore. LIQUi$$|\\rangle $$: A software design architecture and domain-specific language for quantum computing. Available online as arXiv:1402.4467, 2014."},{"key":"6_CR68","doi-asserted-by":"crossref","unstructured":"M.\u00a0Ying. Floyd-hoare logic for quantum programs. ACM Transactions on Programming Languages and Systems (TOPLAS), 33(6):19:1\u201319:49, 2011.","DOI":"10.1145\/2049706.2049708"},{"key":"6_CR69","doi-asserted-by":"crossref","unstructured":"M.\u00a0Ying. Toward automatic verification of quantum programs. Formal Aspects of Computing, 31(1):3\u201325, 2019.","DOI":"10.1007\/s00165-018-0465-3"},{"key":"6_CR70","doi-asserted-by":"crossref","unstructured":"M.\u00a0Ying, Y.\u00a0Li, N.\u00a0Yu, and Y.\u00a0Feng. Model-checking linear-time properties of quantum systems. ACM Transactions on Computational Logic, 15(3):22:1\u201322:31, 2014.","DOI":"10.1145\/2629680"},{"key":"6_CR71","doi-asserted-by":"crossref","unstructured":"M.\u00a0Ying, S.\u00a0Ying, and X.\u00a0Wu. Invariants of quantum programs: characterisations and generation. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2017), pages 818\u2013832, Paris, France, 2017. ACM.","DOI":"10.1145\/3009837.3009840"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-72019-3_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,10,25]],"date-time":"2021-10-25T03:04:22Z","timestamp":1635131062000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-72019-3_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030720186","9783030720193"],"references-count":71,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-72019-3_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"23 March 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ESOP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Symposium on Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 March 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 April 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2021\/esop","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"79","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"24","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"30% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3-5","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"10","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference took place virtually due to the COVID-19 pandemic","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}