[20] Patrick Behm, Paul Benoit, Alain Faivre, and Jean-Marc Meynadier. Météor: A successful application of B in a large project. In *In Proceedings of the World Congress on Formal Methods in the Development of Computing Systems (FM'99)*. Springer, 1999.

[21] John S Bell. On the Einstein Podolsky Rosen paradox. *Physics Physique Fizika*, 1(3):195-200, 1964.

[22] C. H. Bennett and G. Brassard. Quantum cryptography: Public key distribution and coin tossing. In *Proceedings of IEEE International Conference on Computers, Systems and Signal Processing*, pages 175-179, Bangalore, India, 1984.

[23] Nick Benton. A mixed linear and non-linear logic: Proofs, terms and models (extended abstract). In Leszek Pacholski and Jerzy Tiuryn, editors, *Computer Science Logic, Eighth International Workshop, CSL'94, Selected Papers*, volume 933 of *Lecture Notes in Computer Science*, pages 121-135, 1994.

[24] Jort Martinus Bergfeld and Joshua Sack. Deriving the correctness of quantum protocols in the probabilistic logic for quantum programs. *Soft Comput.*, 21(6):1421-1441, 2017.

[25] Yves Bertot and Pierre Castéran. *Interactive theorem proving and program development: Coq'Art: the calculus of inductive constructions*. Springer Science & Business Media, 2013.

[26] Jacob Biamonte, Peter Wittek, Nicola Pancotti, Patrick Rebentrost, Nathan Wiebe, and Seth Lloyd. Quantum machine learning. *Nature*, 549(7671):195, 2017.

[27] Benjamin Bichsel, Maximilian Baader, Timon Gehr, and Martin T. Vechev. Silq: a high-level quantum language with safe uncomputation and intuitive semantics. In Alastair F. Donaldson and Emina Torlak, 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-300. ACM, 2020.

[28] Jaap Boender, Florian Kammüller, and Rajagopal Nagarajan. Formalization of quantum protocols using Coq. In Chris Heunen, Peter Selinger, and Jamie 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-83, Oxford, UK, 2015. EPTCS.

[29] Adam D Bookatz. QMA-complete problems. *Quantum Information & Computation*, 14(5&6):361-383, 2014.

[30] Anthony Bordg, Hanna Lachnitt, and Yijun He. Certified quantum computation in Isabelle/HOL. *Journal of Automated Reasoning*, 65(5):691-709, 2021.

[31] E. Bounimova, P. Godefroid, and D. Molnar. Billions and billions of constraints: Whitebox fuzz testing in production. In *35th International Conference on Software Engineering (ICSE)*, pages 122-131. IEEE/ACM, 2013.

[32] Hans J. Briegel, Dan E. Browne, Wolfgang Dür, Robert Raußendorf, and Maarten Van den Nest. Measurement-based quantum computation. *Nature Physics*, 5(1):19-26, January 2009.

[33] Daniel E Browne, Elham Kashefi, Mehdi Mhalla, and Simon Perdrix. Generalized flow and determinism in measurement-based quantum computation. *New Journal of Physics*, 9(8):250-250, aug 2007.
[20] Patrick Behm, Paul Benoit, Alain Faivre, and Jean-Marc Meynadier. Météor: A successful application of B in a large project. In *In Proceedings of the World Congress on Formal Methods in the Development of Computing Systems (FM'99)*. Springer, 1999.

[21] John S Bell. On the Einstein Podolsky Rosen paradox. *Physics Physique Fizika*, 1(3):195-200, 1964.

[22] C. H. Bennett and G. Brassard. Quantum cryptography: Public key distribution and coin tossing. In *Proceedings of IEEE International Conference on Computers, Systems and Signal Processing*, pages 175-179, Bangalore, India, 1984.

[23] Nick Benton. A mixed linear and non-linear logic: Proofs, terms and models (extended abstract). In Leszek Pacholski and Jerzy Tiuryn, editors, *Computer Science Logic, Eighth International Workshop, CSL'94, Selected Papers*, volume 933 of *Lecture Notes in Computer Science*, pages 121-135, 1994.

[24] Jort Martinus Bergfeld and Joshua Sack. Deriving the correctness of quantum protocols in the probabilistic logic for quantum programs. *Soft Comput.*, 21(6):1421-1441, 2017.

[25] Yves Bertot and Pierre Castéran. *Interactive theorem proving and program development: Coq'Art: the calculus of inductive constructions*. Springer Science & Business Media, 2013.

[26] Jacob Biamonte, Peter Wittek, Nicola Pancotti, Patrick Rebentrost, Nathan Wiebe, and Seth Lloyd. Quantum machine learning. *Nature*, 549(7671):195, 2017.

[27] Benjamin Bichsel, Maximilian Baader, Timon Gehr, and Martin T. Vechev. Silq: a high-level quantum language with safe uncomputation and intuitive semantics. In Alastair F. Donaldson and Emina Torlak, 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-300. ACM, 2020.

[28] Jaap Boender, Florian Kammüller, and Rajagopal Nagarajan. Formalization of quantum protocols using Coq. In Chris Heunen, Peter Selinger, and Jamie 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-83, Oxford, UK, 2015. EPTCS.

[29] Adam D Bookatz. QMA-complete problems. *Quantum Information & Computation*, 14(5&6):361-383, 2014.

[30] Anthony Bordg, Hanna Lachnitt, and Yijun He. Certified quantum computation in Isabelle/HOL. *Journal of Automated Reasoning*, 65(5):691-709, 2021.

[31] E. Bounimova, P. Godefroid, and D. Molnar. Billions and billions of constraints: Whitebox fuzz testing in production. In *35th International Conference on Software Engineering (ICSE)*, pages 122-131. IEEE/ACM, 2013.

[32] Hans J. Briegel, Dan E. Browne, Wolfgang Dür, Robert Raußendorf, and Maarten Van den Nest. Measurement-based quantum computation. *Nature Physics*, 5(1):19-26, January 2009.

[33] Daniel E Browne, Elham Kashefi, Mehdi Mhalla, and Simon Perdrix. Generalized flow and determinism in measurement-based quantum computation. *New Journal of Physics*, 9(8):250-250, aug 2007.
[34] Olivier Brunet and Philippe Jorrand. Dynamic quantum logic for quantum programs. *International Journal of Quantum Information*, 2(01):45-54, 2004.

[35] Cristian Cadar and Koushik Sen. Symbolic execution for software testing: three decades later. *Commun. ACM*, 56(2):82-90, 2013.

[36] Titouan Carette, Emmanuel Jeandel, Simon Perdrix, and Renaud Vilmart. Completeness of Graphical Languages for Mixed States Quantum Mechanics. In Christel Baier, Ioannis Chatzigiannakis, Paola Flocchini, and Stefano Leonardi, editors, *46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)*, volume 132 of *Leibniz International Proceedings in Informatics (LIPIcs)*, pages 108:1-108:15, Dagstuhl, Germany, 2019. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik.

[37] Rohit Chadha, Paulo Mateus, and Amílcar Sernadas. Reasoning about imperative quantum programs. *Electronic Notes in Theoretical Computer Science*, 158:19-39, 2006.

[38] Christophe Chareton, Sébastien Bardin, François Bobot, Valentin Perrelle, and Benoît Valiron. An automated deductive verification framework for circuit-building quantum programs. In Nobuko Yoshida, editor, *Programming Languages and Systems - 30th European Symposium on Programming, ESOP 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings*, volume 12648 of *Lecture Notes in Computer Science*, pages 148-177. Springer, 2021.

[39] Lily Chen, Lily Chen, Stephen Jordan, Yi-Kai Liu, Dustin Moody, Rene Peralta, Ray Perlner, and Daniel Smith-Tone. *Report on post-quantum cryptography*, volume 12. US Department of Commerce, National Institute of Standards and Technology, 2016.

[40] John Chiaverini, Dietrich Leibfried, Tobias Schaetz, Murray D Barrett, RB Blakestad, J Britton, Wayne M Itano, Juergen D Jost, Emanuel Knill, Christopher Langer, et al. Realization of quantum error correction. *Nature*, 432(7017):602-605, 2004.

[41] Cirq Developers. Cirq, July 2018. See full list of authors on Github: https://github.com/quantumlib/Cirq/graphs/contributors.

[42] Edmund M. Clarke and E. Allen Emerson. Design and synthesis of synchronization skeletons using branching-time temporal logic. In *Logics of Programs, Workshop, LNCS 131*, pages 52-71. Springer, 1981.

[43] Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem. *Handbook of Model Checking*. Springer, 2018.

[44] Edmund M. Clarke and Jeannette M. Wing. Formal methods: State of the art and future directions. *ACM Computing Surveys (CSUR)*, 28(4):626-643, 1996.

[45] John F Clauser, Michael A Horne, Abner Shimony, and Richard A Holt. Proposed experiment to test local hidden-variable theories. *Physical review letters*, 23(15):880, 1969.

[46] Bob Coecke and Ross Duncan. Interacting quantum observables: Categorical algebra and diagrammatics. *New Journal of Physics*, 13(4):043016, Apr 2011.

[47] Bob Coecke and Aleks Kissinger. *Picturing quantum processes*. Cambridge University Press, Cambridge, United Kingdom, 2017.
[34] Olivier Brunet and Philippe Jorrand. Dynamic quantum logic for quantum programs. *International Journal of Quantum Information*, 2(01):45-54, 2004.

[35] Cristian Cadar and Koushik Sen. Symbolic execution for software testing: three decades later. *Commun. ACM*, 56(2):82-90, 2013.

[36] Titouan Carette, Emmanuel Jeandel, Simon Perdrix, and Renaud Vilmart. Completeness of Graphical Languages for Mixed States Quantum Mechanics. In Christel Baier, Ioannis Chatzigiannakis, Paola Flocchini, and Stefano Leonardi, editors, *46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)*, volume 132 of *Leibniz International Proceedings in Informatics (LIPIcs)*, pages 108:1-108:15, Dagstuhl, Germany, 2019. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik.

[37] Rohit Chadha, Paulo Mateus, and Amílcar Sernadas. Reasoning about imperative quantum programs. *Electronic Notes in Theoretical Computer Science*, 158:19-39, 2006.

[38] Christophe Chareton, Sébastien Bardin, François Bobot, Valentin Perrelle, and Benoît Valiron. An automated deductive verification framework for circuit-building quantum programs. In Nobuko Yoshida, editor, *Programming Languages and Systems - 30th European Symposium on Programming, ESOP 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings*, volume 12648 of *Lecture Notes in Computer Science*, pages 148-177. Springer, 2021.

[39] Lily Chen, Lily Chen, Stephen Jordan, Yi-Kai Liu, Dustin Moody, Rene Peralta, Ray Perlner, and Daniel Smith-Tone. *Report on post-quantum cryptography*, volume 12. US Department of Commerce, National Institute of Standards and Technology, 2016.

[40] John Chiaverini, Dietrich Leibfried, Tobias Schaetz, Murray D Barrett, RB Blakestad, J Britton, Wayne M Itano, Juergen D Jost, Emanuel Knill, Christopher Langer, et al. Realization of quantum error correction. *Nature*, 432(7017):602-605, 2004.

[41] Cirq Developers. Cirq, July 2018. See full list of authors on Github: https://github.com/quantumlib/Cirq/graphs/contributors.

[42] Edmund M. Clarke and E. Allen Emerson. Design and synthesis of synchronization skeletons using branching-time temporal logic. In *Logics of Programs, Workshop, LNCS 131*, pages 52-71. Springer, 1981.

[43] Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem. *Handbook of Model Checking*. Springer, 2018.

[44] Edmund M. Clarke and Jeannette M. Wing. Formal methods: State of the art and future directions. *ACM Computing Surveys (CSUR)*, 28(4):626-643, 1996.

[45] John F Clauser, Michael A Horne, Abner Shimony, and Richard A Holt. Proposed experiment to test local hidden-variable theories. *Physical review letters*, 23(15):880, 1969.

[46] Bob Coecke and Ross Duncan. Interacting quantum observables: Categorical algebra and diagrammatics. *New Journal of Physics*, 13(4):043016, Apr 2011.

[47] Bob Coecke and Aleks Kissinger. *Picturing quantum processes*. Cambridge University Press, Cambridge, United Kingdom, 2017.
[48] Bob Coecke and Simon Perdrix. Environment and classical channels in categorical quantum mechanics. *Log. Methods Comput. Sci.*, 8(4), 2010.

[49] Patrick Cousot and Radhia Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In *Proceedings of the Fourth ACM Symposium on Principles of Programming Languages (POPL)*, pages 238–252. ACM, 1977.

[50] Patrick Cousot, Radhia Cousot, Jerôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, and Xavier Rival. The ASTRÉE analyzer. In *European Symposium on Programming Languages and Systems, ESOP 2005*. Springer, 2005.

[51] Andrew W. Cross, Lev S. Bishop, John A. Smolin, and Jay M. Gambetta. Open quantum assembly language, 2017.

[52] Vincent Danos and Elham Kashefi. Determinism in the one-way model. *Phys. Rev. A*, 74:052310, Nov 2006.

[53] Niel de Beaudrap, Xiaoning Bian, and Quanlong Wang. Fast and effective techniques for T-count reduction via spider nest identities. In Steven T. Flammia, editor, *15th Conference on the Theory of Quantum Computation, Communication and Cryptography, TQC 2020, June 9-12, 2020, Riga, Latvia*, volume 158 of *LIPIcs*, pages 11:1–11:23. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020.

[54] Niel de Beaudrap, Ross Duncan, Dominic Horsman, and Simon Perdrix. Pauli fusion: a computational model to realise quantum transformations from ZX terms. In *QPL’19 : International Conference on Quantum Physics and Logic*, Los Angeles, United States, June 2019.

[55] Niel de Beaudrap and Dominic Horsman. The ZX calculus is a language for surface code lattice surgery. *Quantum*, 4:218, January 2020.

[56] Ellie D’Hondt and Prakash Panangaden. Quantum weakest preconditions. *Mathematical Structures in Computer Science*, 16(3):429–451, 2006.

[57] Alejandro Díaz-Caro. A lambda calculus for density matrices with classical and probabilistic controls. In Bor-Yuh Evan Chang, editor, *Proceedings of the 15th Asian Symposium on Programming Languages and Systems (APLAS’17)*, volume 10695 of *Lecture Notes in Computer Science*, pages 448–467, Suzhou, China, 2017. Springer.

[58] Alejandro Díaz-Caro and Octavio Malherbe. A concrete categorical semantics of lambdas. In Beniamino Accattoli and Carlos Olarte, editors, *Proceedings of the 13th Workshop on Logical and Semantic Frameworks with Applications, LSFA 2018, Fortaleza, Brazil, September 26-28, 2018*, volume 344 of *Electronic Notes in Theoretical Computer Science*, pages 83–100. Elsevier, 2019.

[59] Edsger W. Dijkstra. *A Discipline of Programming*. Prentice-Hall, 1976.

[60] Ross Duncan, Aleks Kissinger, Simon Perdrix, and John van de Wetering. Graph-theoretic simplification of quantum circuits with the ZX-calculus. *Quantum*, 4:279, 2020.

[61] Mnacho Echenim. Quantum projective measurements and the CHSH inequality. *Arch. Formal Proofs*, 2021, 2021.
[48] Bob Coecke and Simon Perdrix. Environment and classical channels in categorical quantum mechanics. *Log. Methods Comput. Sci.*, 8(4), 2010.

[49] Patrick Cousot and Radhia Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In *Proceedings of the Fourth ACM Symposium on Principles of Programming Languages (POPL)*, pages 238–252. ACM, 1977.

[50] Patrick Cousot, Radhia Cousot, Jerôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, and Xavier Rival. The ASTRÉE analyzer. In *European Symposium on Programming Languages and Systems, ESOP 2005*. Springer, 2005.

[51] Andrew W. Cross, Lev S. Bishop, John A. Smolin, and Jay M. Gambetta. Open quantum assembly language, 2017.

[52] Vincent Danos and Elham Kashefi. Determinism in the one-way model. *Phys. Rev. A*, 74:052310, Nov 2006.

[53] Niel de Beaudrap, Xiaoning Bian, and Quanlong Wang. Fast and effective techniques for T-count reduction via spider nest identities. In Steven T. Flammia, editor, *15th Conference on the Theory of Quantum Computation, Communication and Cryptography, TQC 2020, June 9-12, 2020, Riga, Latvia*, volume 158 of *LIPIcs*, pages 11:1–11:23. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020.

[54] Niel de Beaudrap, Ross Duncan, Dominic Horsman, and Simon Perdrix. Pauli fusion: a computational model to realise quantum transformations from ZX terms. In *QPL’19 : International Conference on Quantum Physics and Logic*, Los Angeles, United States, June 2019.

[55] Niel de Beaudrap and Dominic Horsman. The ZX calculus is a language for surface code lattice surgery. *Quantum*, 4:218, January 2020.

[56] Ellie D’Hondt and Prakash Panangaden. Quantum weakest preconditions. *Mathematical Structures in Computer Science*, 16(3):429–451, 2006.

[57] Alejandro Díaz-Caro. A lambda calculus for density matrices with classical and probabilistic controls. In Bor-Yuh Evan Chang, editor, *Proceedings of the 15th Asian Symposium on Programming Languages and Systems (APLAS’17)*, volume 10695 of *Lecture Notes in Computer Science*, pages 448–467, Suzhou, China, 2017. Springer.

[58] Alejandro Díaz-Caro and Octavio Malherbe. A concrete categorical semantics of lambdas. In Beniamino Accattoli and Carlos Olarte, editors, *Proceedings of the 13th Workshop on Logical and Semantic Frameworks with Applications, LSFA 2018, Fortaleza, Brazil, September 26-28, 2018*, volume 344 of *Electronic Notes in Theoretical Computer Science*, pages 83–100. Elsevier, 2019.

[59] Edsger W. Dijkstra. *A Discipline of Programming*. Prentice-Hall, 1976.

[60] Ross Duncan, Aleks Kissinger, Simon Perdrix, and John van de Wetering. Graph-theoretic simplification of quantum circuits with the ZX-calculus. *Quantum*, 4:279, 2020.

[61] Mnacho Echenim. Quantum projective measurements and the CHSH inequality. *Arch. Formal Proofs*, 2021, 2021.
[62] Albert Einstein, Boris Podolsky, and Nathan Rosen. Can quantum-mechanical description of physical reality be considered complete? *Physical review*, 47(10):777, 1935.

[63] Mohamed Elboukhari, Mostafa Azizi, and Abdelmalek Azizi. Verification of quantum crypography protocols by model checking. *Int. J. Network Security & Appl*, 2(4):43–53, 2010.

[64] Edward Farhi, Jeffrey Goldstone, and Sam Gutmann. A quantum approximate optimization algorithm. Technical Report MIT-CTP/4610, MIT, 2014.

[65] Edward Farhi, Jeffrey Goldstone, Sam Gutmann, Joshua Lapan, Andrew Lundgren, and Daniel Preda. A quantum adiabatic evolution algorithm applied to random instances of an np-complete problem. *Science*, 292(5516):472–475, 2001.

[66] Yuan Feng, Runyao Duan, Zhengfeng Ji, and Mingsheng Ying. Proof rules for the correctness of quantum programs. *Theoretical Computer Science*, 386(1-2):151–166, 2007.

[67] Yuan Feng and Mingsheng Ying. Quantum hoare logic with classical variables. CoRR, abs/2008.06812, 2020.

[68] Verónica Fernández, María-José García-Martínez, Luis Hernández-Encinas, and Agustín Martín. Formal verification of the security of a free-space quantum key distribution system. In *Proc. World Congr. Comput. Sci. Comput. Eng. Appl. Comput. (WORLDCOMP) Int. Conf. Security Manag. (SAM)*, 2011.

[69] Richard P. Feynman. Simulating physics with computers. *International Journal of Theoretical Physics*, 21(6-7):467–488, 1982.

[70] Jean-Christophe Filliâtre and Andrei Paskevich. Why3 - where programs meet provers. In Matthias Felleisen and Philippa Gardner, 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–128, Rome, Italy, 2013. Springer.

[71] Jean-Christophe Filliâtre. Deductive software verification. STTT, 13(5):397–403, 2011.

[72] Michael J Fischer and Richard E Ladner. Propositional dynamic logic of regular programs. *Journal of computer and system sciences*, 18(2):194–211, 1979.

[73] Melvin Fitting. *First-order logic and automated theorem proving*. Springer Science & Business Media, 2012.

[74] R. W. Floyd. Assigning meanings to programs. In *Mathematical Aspects of Computer Science, Proceedings of Symposia in Applied Mathematics*, pages 19–32. American Mathematical Society, 1967.

[75] Austin G. Fowler, Matteo Mariantoni, John M. Martinis, and Andrew N. Cleland. Surface codes: Towards practical large-scale quantum computation. *Phys. Rev. A*, 86:032324, Sep 2012.

[76] Michael Freedman, Alexei Kitaev, Michael Larsen, and Zhenghan Wang. Topological quantum computation. *Bulletin of the American Mathematical Society*, 40(1):31–38, 2003.
[62] Albert Einstein, Boris Podolsky, and Nathan Rosen. Can quantum-mechanical description of physical reality be considered complete? *Physical review*, 47(10):777, 1935.

[63] Mohamed Elboukhari, Mostafa Azizi, and Abdelmalek Azizi. Verification of quantum crypography protocols by model checking. *Int. J. Network Security & Appl*, 2(4):43–53, 2010.

[64] Edward Farhi, Jeffrey Goldstone, and Sam Gutmann. A quantum approximate optimization algorithm. Technical Report MIT-CTP/4610, MIT, 2014.

[65] Edward Farhi, Jeffrey Goldstone, Sam Gutmann, Joshua Lapan, Andrew Lundgren, and Daniel Preda. A quantum adiabatic evolution algorithm applied to random instances of an np-complete problem. *Science*, 292(5516):472–475, 2001.

[66] Yuan Feng, Runyao Duan, Zhengfeng Ji, and Mingsheng Ying. Proof rules for the correctness of quantum programs. *Theoretical Computer Science*, 386(1-2):151–166, 2007.

[67] Yuan Feng and Mingsheng Ying. Quantum hoare logic with classical variables. CoRR, abs/2008.06812, 2020.

[68] Verónica Fernández, María-José García-Martínez, Luis Hernández-Encinas, and Agustín Martín. Formal verification of the security of a free-space quantum key distribution system. In *Proc. World Congr. Comput. Sci. Comput. Eng. Appl. Comput. (WORLDCOMP) Int. Conf. Security Manag. (SAM)*, 2011.

[69] Richard P. Feynman. Simulating physics with computers. *International Journal of Theoretical Physics*, 21(6-7):467–488, 1982.

[70] Jean-Christophe Filliâtre and Andrei Paskevich. Why3 - where programs meet provers. In Matthias Felleisen and Philippa Gardner, 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–128, Rome, Italy, 2013. Springer.

[71] Jean-Christophe Filliâtre. Deductive software verification. STTT, 13(5):397–403, 2011.

[72] Michael J Fischer and Richard E Ladner. Propositional dynamic logic of regular programs. *Journal of computer and system sciences*, 18(2):194–211, 1979.

[73] Melvin Fitting. *First-order logic and automated theorem proving*. Springer Science & Business Media, 2012.

[74] R. W. Floyd. Assigning meanings to programs. In *Mathematical Aspects of Computer Science, Proceedings of Symposia in Applied Mathematics*, pages 19–32. American Mathematical Society, 1967.

[75] Austin G. Fowler, Matteo Mariantoni, John M. Martinis, and Andrew N. Cleland. Surface codes: Towards practical large-scale quantum computation. *Phys. Rev. A*, 86:032324, Sep 2012.

[76] Michael Freedman, Alexei Kitaev, Michael Larsen, and Zhenghan Wang. Topological quantum computation. *Bulletin of the American Mathematical Society*, 40(1):31–38, 2003.
[77] Peng Fu, Kohei Kishida, and Peter Selinger. Linear dependent type theory for quantum programming languages. In *Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science*, pages 440–453, 2020.

[78] Simon J. Gay, Rajagopal Nagarajan, and Nikolaos Papanikolaou. QMC: a model checker for quantum systems. In Aarti Gupta and Sharad Malik, editors, *Proceeding of the 20th International Conference on Computer Aided Verification (CAV 2008)*, volume 5123 of *Lecture Notes in Computer Science*, pages 543–547, Princeton, NJ, USA, 2008. Springer.

[79] Jean-Yves Girard. Linear logic. *Theoretical Computer Science*, 50(1):1–101, 1987.

[80] Georges Gonthier. Formal proof – the four-color theorem. *Notices of the AMS*, 55(11):1382–1393, 2008.

[81] Daniel Gottesman. *Stabilizer codes and quantum error correction*. PhD thesis, Caltech, 1997.

[82] Alexander S. Green, Peter LeFanu Lumsdaine, Neil J. Ross, Peter Selinger, and Benoît Valiron. An introduction to quantum programming in Quipper. In Gerhard W. Dueck and D. Michael Miller, editors, *Proceedings of the 5th International Conference on Reversible Computation (RC’13)*, volume 7948 of *Lecture Notes in Computer Science*, pages 110–124, Victoria, BC, Canada, 2013. Springer.

[83] Alexander S. Green, Peter LeFanu Lumsdaine, Neil J. Ross, Peter Selinger, and Benoît Valiron. Quipper: A scalable quantum programming language. In Hans-Juergen Boehm and Cormac Flanagan, editors, *Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, (PLDI’13)*, pages 333–342, Seattle, WA, USA, 2013. ACM.

[84] Lov K. Grover. A fast quantum mechanical algorithm for database search. In Gary L. Miller, editor, *Proceedings of the Twenty-Eighth Annual ACM Symposium on the Theory of Computing (STOC)*, pages 212–219, Philadelphia, Pennsylvania, USA, 1996. ACM.

[85] Amar Hadzihasanovic, Kang Feng Ng, and Quanlong Wang. Two complete axiomatisations of pure-state qubit quantum computing. In *Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science*, LICS ’18, pages 502–511, New York, NY, USA, 2018. ACM.

[86] David Harel, Dexter Kozen, and Jerzy Tiuryn. Dynamic logic. In *Handbook of philosophical logic*, pages 99–217. Springer, 2001.

[87] Aram W. Harrow, Avinatan Hassidim, and Seth Lloyd. Quantum algorithm for linear systems of equations. *Physical Review Letters*, 103:150502, Oct 2009.

[88] Ichiro Hasuo and Naohiko Hoshino. Semantics of higher-order quantum computation via geometry of interaction. *Annals of Pure and Applied Logic*, 168(2):404 – 469, 2017.

[89] Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, and Grégoire Sutre. Software verification with Blast. In *Proceedings of the 10th International Conference on Model Checking Software, SPIN’03*. Springer, 2003.

[90] Kesha Hietala, Robert Rand, Shih-Han Hung, Liyi Li, and Michael Hicks. Proving quantum programs correct. In Liron Cohen and Cezary Kaliszyk, editors, *12th International Conference on Interactive Theorem Proving, ITP 2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)*, volume 193 of *LIPIcs*, pages 21:1–21:19, 2021.
[77] Peng Fu, Kohei Kishida, and Peter Selinger. Linear dependent type theory for quantum programming languages. In *Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science*, pages 440–453, 2020.

[78] Simon J. Gay, Rajagopal Nagarajan, and Nikolaos Papanikolaou. QMC: a model checker for quantum systems. In Aarti Gupta and Sharad Malik, editors, *Proceeding of the 20th International Conference on Computer Aided Verification (CAV 2008)*, volume 5123 of *Lecture Notes in Computer Science*, pages 543–547, Princeton, NJ, USA, 2008. Springer.

[79] Jean-Yves Girard. Linear logic. *Theoretical Computer Science*, 50(1):1–101, 1987.

[80] Georges Gonthier. Formal proof – the four-color theorem. *Notices of the AMS*, 55(11):1382–1393, 2008.

[81] Daniel Gottesman. *Stabilizer codes and quantum error correction*. PhD thesis, Caltech, 1997.

[82] Alexander S. Green, Peter LeFanu Lumsdaine, Neil J. Ross, Peter Selinger, and Benoît Valiron. An introduction to quantum programming in Quipper. In Gerhard W. Dueck and D. Michael Miller, editors, *Proceedings of the 5th International Conference on Reversible Computation (RC’13)*, volume 7948 of *Lecture Notes in Computer Science*, pages 110–124, Victoria, BC, Canada, 2013. Springer.

[83] Alexander S. Green, Peter LeFanu Lumsdaine, Neil J. Ross, Peter Selinger, and Benoît Valiron. Quipper: A scalable quantum programming language. In Hans-Juergen Boehm and Cormac Flanagan, editors, *Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, (PLDI’13)*, pages 333–342, Seattle, WA, USA, 2013. ACM.

[84] Lov K. Grover. A fast quantum mechanical algorithm for database search. In Gary L. Miller, editor, *Proceedings of the Twenty-Eighth Annual ACM Symposium on the Theory of Computing (STOC)*, pages 212–219, Philadelphia, Pennsylvania, USA, 1996. ACM.

[85] Amar Hadzihasanovic, Kang Feng Ng, and Quanlong Wang. Two complete axiomatisations of pure-state qubit quantum computing. In *Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science*, LICS ’18, pages 502–511, New York, NY, USA, 2018. ACM.

[86] David Harel, Dexter Kozen, and Jerzy Tiuryn. Dynamic logic. In *Handbook of philosophical logic*, pages 99–217. Springer, 2001.

[87] Aram W. Harrow, Avinatan Hassidim, and Seth Lloyd. Quantum algorithm for linear systems of equations. *Physical Review Letters*, 103:150502, Oct 2009.

[88] Ichiro Hasuo and Naohiko Hoshino. Semantics of higher-order quantum computation via geometry of interaction. *Annals of Pure and Applied Logic*, 168(2):404 – 469, 2017.

[89] Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, and Grégoire Sutre. Software verification with Blast. In *Proceedings of the 10th International Conference on Model Checking Software, SPIN’03*. Springer, 2003.

[90] Kesha Hietala, Robert Rand, Shih-Han Hung, Liyi Li, and Michael Hicks. Proving quantum programs correct. In Liron Cohen and Cezary Kaliszyk, editors, *12th International Conference on Interactive Theorem Proving, ITP 2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)*, volume 193 of *LIPIcs*, pages 21:1–21:19, 2021.
[91] Kesha Hietala, Robert Rand, Shih-Han Hung, Xiaodi Wu, and Michael Hicks. A verified optimizer for quantum circuits. *Proc. ACM Program. Lang.*, 5(POPL):1–29, 2021.

[92] Anne Hillebrand. Quantum protocols involving multiparticle entanglement and their representations. Master's thesis, University of Oxford, 2011.

[93] R. Hindley. The principal type-scheme of an object in combinatory logic. *Transactions of the American Mathematical Society*, 146:29–60, 1969.

[94] C. A. R. Hoare. An axiomatic basis for computer programming. *Commun. ACM*, 12(10):576–580, 1969.

[95] Clare Horsman, Austin G. Fowler, Simon Devitt, and Rodney Van Meter. Surface code quantum computing by lattice surgery. *New Journal of Physics*, 14(12):123011, December 2012.

[96] Yipeng Huang and Margaret Martonosi. Statistical assertions for validating patterns and finding bugs in quantum programs. In Srilatha Bobbie Manne, Hillery C. Hunter, and Erik R. Altman, editors, *Proceedings of the 46th International Symposium on Computer Architecture (ISCA 2019)*, pages 541–553, Phoenix, AZ, USA, 2019. ACM.

[97] Shih-Han Hung, Kesha Hietala, Shaopeng Zhu, Mingsheng Ying, Michael Hicks, and Xiaodi Wu. Quantitative robustness analysis of quantum programs. *Proceedings of the ACM on Programming Languages*, 3(POPL):1–29, 2019.

[98] Dominik Janzing, Pawel Wocjan, and Thomas Beth. "non-identity-check" is QMA-complete. *International Journal of Quantum Information*, 03(03):463–473, 2005.

[99] Ali JavadiAbhari, Shruti Patil, Daniel Kudrow, Jeff Heckey, Alexey Lvov, Frederic T. Chong, and Margaret Martonosi. ScaffCC: Scalable compilation and analysis of quantum programs. *Parallel Computing*, 45:2–17, 2015.

[100] Emmanuel Jeandel. The rational fragment of the ZX-calculus, 2018.

[101] Emmanuel Jeandel, Simon Perdrix, and Renaud Vilmart. A complete axiomatisation of the ZX-calculus for Clifford+T quantum mechanics. In *Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science*, LICS '18, pages 559–568, New York, NY, USA, 2018. ACM.

[102] Emmanuel Jeandel, Simon Perdrix, and Renaud Vilmart. Diagrammatic reasoning beyond Clifford+T quantum mechanics. In *Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science*, LICS '18, pages 569–578, New York, NY, USA, 2018. ACM.

[103] Emmanuel Jeandel, Simon Perdrix, and Renaud Vilmart. A generic normal form for ZX-diagrams and application to the rational angle completeness. In *2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)*, pages 1–10, 2019.

[104] Emmanuel Jeandel, Simon Perdrix, and Renaud Vilmart. Completeness of the ZX-calculus. *Logical Methods in Computer Science*, 16(2), 2020.

[105] Yoshihiko Kakutani. A logic for formal verification of quantum programs. In *Annual Asian Computing Science Conference*, pages 79–93. Springer, 2009.
[91] Kesha Hietala, Robert Rand, Shih-Han Hung, Xiaodi Wu, and Michael Hicks. A verified optimizer for quantum circuits. *Proc. ACM Program. Lang.*, 5(POPL):1–29, 2021.

[92] Anne Hillebrand. Quantum protocols involving multiparticle entanglement and their representations. Master's thesis, University of Oxford, 2011.

[93] R. Hindley. The principal type-scheme of an object in combinatory logic. *Transactions of the American Mathematical Society*, 146:29–60, 1969.

[94] C. A. R. Hoare. An axiomatic basis for computer programming. *Commun. ACM*, 12(10):576–580, 1969.

[95] Clare Horsman, Austin G. Fowler, Simon Devitt, and Rodney Van Meter. Surface code quantum computing by lattice surgery. *New Journal of Physics*, 14(12):123011, December 2012.

[96] Yipeng Huang and Margaret Martonosi. Statistical assertions for validating patterns and finding bugs in quantum programs. In Srilatha Bobbie Manne, Hillery C. Hunter, and Erik R. Altman, editors, *Proceedings of the 46th International Symposium on Computer Architecture (ISCA 2019)*, pages 541–553, Phoenix, AZ, USA, 2019. ACM.

[97] Shih-Han Hung, Kesha Hietala, Shaopeng Zhu, Mingsheng Ying, Michael Hicks, and Xiaodi Wu. Quantitative robustness analysis of quantum programs. *Proceedings of the ACM on Programming Languages*, 3(POPL):1–29, 2019.

[98] Dominik Janzing, Pawel Wocjan, and Thomas Beth. “non-identity-check” is QMA-complete. *International Journal of Quantum Information*, 03(03):463–473, 2005.

[99] Ali JavadiAbhari, Shruti Patil, Daniel Kudrow, Jeff Heckey, Alexey Lvov, Frederic T. Chong, and Margaret Martonosi. ScaffCC: Scalable compilation and analysis of quantum programs. *Parallel Computing*, 45:2–17, 2015.

[100] Emmanuel Jeandel. The rational fragment of the ZX-calculus, 2018.

[101] Emmanuel Jeandel, Simon Perdrix, and Renaud Vilmart. A complete axiomatisation of the ZX-calculus for Clifford+T quantum mechanics. In *Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science*, LICS '18, pages 559–568, New York, NY, USA, 2018. ACM.

[102] Emmanuel Jeandel, Simon Perdrix, and Renaud Vilmart. Diagrammatic reasoning beyond Clifford+T quantum mechanics. In *Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science*, LICS '18, pages 569–578, New York, NY, USA, 2018. ACM.

[103] Emmanuel Jeandel, Simon Perdrix, and Renaud Vilmart. A generic normal form for ZX-diagrams and application to the rational angle completeness. In *2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)*, pages 1–10, 2019.

[104] Emmanuel Jeandel, Simon Perdrix, and Renaud Vilmart. Completeness of the ZX-calculus. *Logical Methods in Computer Science*, 16(2), 2020.

[105] Yoshihiko Kakutani. A logic for formal verification of quantum programs. In *Annual Asian Computing Science Conference*, pages 79–93. Springer, 2009.
[106] Nathan Killoran, Josh Izaac, Nicolás Quesada, Ville Bergholm, Matthew Amy, and Christian Weedbrook. Strawberry Fields: A software platform for photonic quantum computing. *Quantum*, 3:129, 2019.

[107] Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles, and Boris Yakobowski. Frama-C: A software analysis perspective. *Formal Asp. Comput.*, 27(3):573-609, 2015.

[108] Aleks Kissinger and John van de Wetering. PyZX: Large scale automated diagrammatic reasoning. *Electronic Proceedings in Theoretical Computer Science*, 318:229-241, May 2020.

[109] Aleks Kissinger and John van de Wetering. Reducing the number of non-clifford gates in quantum circuits. *Phys. Rev. A*, 102:022406, Aug 2020.

[110] Aleks Kissinger and Vladimir Zamdzhiev. Quantomatic: A proof assistant for diagrammatic reasoning. In *Amy P. Felty and Aart Middeldorp, editors, Proceedings for the 25th International Conference on Automated Deduction (CADE-25), volume 9195 of Lecture Notes in Computer Science*, pages 326-336, Berlin, Germany, 2015. Springer.

[111] A Yu Kitaev. Quantum measurements and the abelian stabilizer problem. Available online as arXiv:quant-ph/9511026, 1995.

[112] Erwin Klein, June Andronick, Kevin Elphinstone, Gernot Heiser, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. seL4: formal verification of an operating-system kernel. *Commun. ACM*, 53(6):107-115, 2010.

[113] Emmanuel Knill. Conventions for quantum pseudocode. Technical Report LA-UR-96-2724, Los Alamos National Laboratory, June 1996.

[114] Dexter Kozen. Results on the propositional μ-calculus. *Theoretical computer science*, 27(3):333-354, 1983.

[115] Saul A. Kripke. Semantical considerations on modal logic. *Acta Philosophica Fennica*, 16:83-94, 1963.

[116] Daniel Kroening and Michael Tautschnig. Cbmc - c bounded model checker. In *Tools and Algorithms for the Construction and Analysis of Systems - 20th International Conference, TACAS 2014*, pages 389-391. Springer, 2014.

[117] Takahiro Kubota, Yoshihiko Kakutani, Go Kato, Yasuhito Kawano, and Hideki Sakurada. Semi-automated verification of security proofs of quantum cryptographic protocols. *Journal of Symbolic Computation*, 73:192-220, 2016.

[118] Hidenori Kuwakado and Masakatu Morii. Quantum distinguisher between the 3-round Feistel cipher and the random permutation. In *2010 IEEE International Symposium on Information Theory*, pages 2682-2685. IEEE, 2010.

[119] Hidenori Kuwakado and Masakatu Morii. Security on the quantum-type Even-Mansour cipher. In *2012 International Symposium on Information Theory and its Applications*, pages 312-316. IEEE, 2012.
[106] Nathan Killoran, Josh Izaac, Nicolás Quesada, Ville Bergholm, Matthew Amy, and Christian Weedbrook. Strawberry Fields: A software platform for photonic quantum computing. *Quantum*, 3:129, 2019.

[107] Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles, and Boris Yakobowski. Frama-C: A software analysis perspective. *Formal Asp. Comput.*, 27(3):573-609, 2015.

[108] Aleks Kissinger and John van de Wetering. PyZX: Large scale automated diagrammatic reasoning. *Electronic Proceedings in Theoretical Computer Science*, 318:229-241, May 2020.

[109] Aleks Kissinger and John van de Wetering. Reducing the number of non-clifford gates in quantum circuits. *Phys. Rev. A*, 102:022406, Aug 2020.

[110] Aleks Kissinger and Vladimir Zamdzhiev. Quantomatic: A proof assistant for diagrammatic reasoning. In *Amy P. Felty and Aart Middeldorp, editors, Proceedings for the 25th International Conference on Automated Deduction (CADE-25), volume 9195 of Lecture Notes in Computer Science*, pages 326-336, Berlin, Germany, 2015. Springer.

[111] A Yu Kitaev. Quantum measurements and the abelian stabilizer problem. Available online as arXiv:quant-ph/9511026, 1995.

[112] Erwin Klein, June Andronick, Kevin Elphinstone, Gernot Heiser, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. seL4: formal verification of an operating-system kernel. *Commun. ACM*, 53(6):107-115, 2010.

[113] Emmanuel Knill. Conventions for quantum pseudocode. Technical Report LA-UR-96-2724, Los Alamos National Laboratory, June 1996.

[114] Dexter Kozen. Results on the propositional μ-calculus. *Theoretical computer science*, 27(3):333-354, 1983.

[115] Saul A. Kripke. Semantical considerations on modal logic. *Acta Philosophica Fennica*, 16:83-94, 1963.

[116] Daniel Kroening and Michael Tautschnig. Cbmc - c bounded model checker. In *Tools and Algorithms for the Construction and Analysis of Systems - 20th International Conference, TACAS 2014*, pages 389-391. Springer, 2014.

[117] Takahiro Kubota, Yoshihiko Kakutani, Go Kato, Yasuhito Kawano, and Hideki Sakurada. Semi-automated verification of security proofs of quantum cryptographic protocols. *Journal of Symbolic Computation*, 73:192-220, 2016.

[118] Hidenori Kuwakado and Masakatu Morii. Quantum distinguisher between the 3-round Feistel cipher and the random permutation. In *2010 IEEE International Symposium on Information Theory*, pages 2682-2685. IEEE, 2010.

[119] Hidenori Kuwakado and Masakatu Morii. Security on the quantum-type Even-Mansour cipher. In *2012 International Symposium on Information Theory and its Applications*, pages 312-316. IEEE, 2012.
[120] Ugo Dal Lago, Claudia Faggian, Benoît Valiron, and Akira Yoshimizu. The geometry of parallelism: classical, probabilistic, and quantum effects. In Giuseppe Castagna and Andrew D. Gordon, editors, *Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL'17)*, pages 833–845, Paris, France, 2017. ACM.

[121] Joachim Lambek. The mathematics of sentence structure. *The American Mathematical Monthly*, 65(3):154–170, 1958.

[122] Martin Lange. Model checking propositional dynamic logic with all extras. *Journal of Applied Logic*, 4(1):39–49, 2006.

[123] Louis Lemonnier, John van de Wetering, and Aleks Kissinger. Hypergraph simplification: Linking the path-sum approach to the ZH-calculus. *arXiv preprint arXiv:2003.13564*, 2020.

[124] Xavier Leroy. Formal verification of a realistic compiler. *Commun. ACM*, 52(7):107–115, 2009.

[125] Jerzy Lewandowski. Volume and quantizations. *Classical and Quantum Gravity*, 14(1):71, 1997.

[126] Gushu Li, Li Zhou, Nengkun Yu, Yufei Ding, Mingsheng Ying, and Yuan Xie. Projection-based runtime assertions for testing and debugging quantum programs. *Proceedings of the ACM on Programming Languages*, 4(OOPSLA):1–29, 2020.

[127] Yangjia Li and Mingsheng Ying. Algorithmic analysis of termination problems for quantum programs. *Proceedings of the ACM on Programming Languages*, 2(POPL):1–29, 2017.

[128] Sheng-Kai Liao, Wen-Qi Cai, Wei-Yue Liu, Liang Zhang, Yang Li, Ji-Gang Ren, Juan Yin, Qi Shen, Yuan Cao, Zheng-Ping Li, et al. Satellite-to-ground quantum key distribution. *Nature*, 549(7670):43–47, 2017.

[129] Daniel A Lidar and Todd A Brun. *Quantum Error Correction*. Cambridge University Press, 2013.

[130] Bert Lindenhovius, Michael Mislove, and Vladimir Zamdzhiev. Enriching a linear/non-linear lambda calculus: A programming language for string diagrams. In *Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science*, pages 659–668, 2018.

[131] Junyi Liu, Bohua Zhan, Shuling Wang, Shenggang Ying, Tao Liu, Yangjia Li, Mingsheng Ying, and Naijun Zhan. Formal verification of quantum algorithms using quantum Hoare logic. In Isil Dillig and Serdar Tasiran, editors, *Computer Aided Verification*, pages 187–207, Cham, 2019. Springer International Publishing.

[132] Tao Liu, Yangjia Li, Shuling Wang, Mingsheng Ying, and Naijun Zhan. A theorem prover for quantum Hoare logic and its applications. Available as arXiv:1601.03835, 2016.

[133] Seth Lloyd, Masoud Mohseni, and Patrick Rebentrost. Quantum algorithms for supervised and unsupervised machine learning. *arXiv preprint arXiv:1307.0411*, 2013.

[134] Hoi-Kwong Lo, Xiongfeng Ma, and Kai Chen. Decoy state quantum key distribution. *Physical review letters*, 94(23):230504, 2005.
[120] Ugo Dal Lago, Claudia Faggian, Benoît Valiron, and Akira Yoshimizu. The geometry of parallelism: classical, probabilistic, and quantum effects. In Giuseppe Castagna and Andrew D. Gordon, editors, *Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL'17)*, pages 833–845, Paris, France, 2017. ACM.

[121] Joachim Lambek. The mathematics of sentence structure. *The American Mathematical Monthly*, 65(3):154–170, 1958.

[122] Martin Lange. Model checking propositional dynamic logic with all extras. *Journal of Applied Logic*, 4(1):39–49, 2006.

[123] Louis Lemonnier, John van de Wetering, and Aleks Kissinger. Hypergraph simplification: Linking the path-sum approach to the ZH-calculus. *arXiv preprint arXiv:2003.13564*, 2020.

[124] Xavier Leroy. Formal verification of a realistic compiler. *Commun. ACM*, 52(7):107–115, 2009.

[125] Jerzy Lewandowski. Volume and quantizations. *Classical and Quantum Gravity*, 14(1):71, 1997.

[126] Gushu Li, Li Zhou, Nengkun Yu, Yufei Ding, Mingsheng Ying, and Yuan Xie. Projection-based runtime assertions for testing and debugging quantum programs. *Proceedings of the ACM on Programming Languages*, 4(OOPSLA):1–29, 2020.

[127] Yangjia Li and Mingsheng Ying. Algorithmic analysis of termination problems for quantum programs. *Proceedings of the ACM on Programming Languages*, 2(POPL):1–29, 2017.

[128] Sheng-Kai Liao, Wen-Qi Cai, Wei-Yue Liu, Liang Zhang, Yang Li, Ji-Gang Ren, Juan Yin, Qi Shen, Yuan Cao, Zheng-Ping Li, et al. Satellite-to-ground quantum key distribution. *Nature*, 549(7670):43–47, 2017.

[129] Daniel A Lidar and Todd A Brun. *Quantum Error Correction*. Cambridge University Press, 2013.

[130] Bert Lindenhovius, Michael Mislove, and Vladimir Zamdzhiev. Enriching a linear/non-linear lambda calculus: A programming language for string diagrams. In *Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science*, pages 659–668, 2018.

[131] Junyi Liu, Bohua Zhan, Shuling Wang, Shenggang Ying, Tao Liu, Yangjia Li, Mingsheng Ying, and Naijun Zhan. Formal verification of quantum algorithms using quantum Hoare logic. In Isil Dillig and Serdar Tasiran, editors, *Computer Aided Verification*, pages 187–207, Cham, 2019. Springer International Publishing.

[132] Tao Liu, Yangjia Li, Shuling Wang, Mingsheng Ying, and Naijun Zhan. A theorem prover for quantum Hoare logic and its applications. Available as arXiv:1601.03835, 2016.

[133] Seth Lloyd, Masoud Mohseni, and Patrick Rebentrost. Quantum algorithms for supervised and unsupervised machine learning. *arXiv preprint arXiv:1307.0411*, 2013.

[134] Hoi-Kwong Lo, Xiongfeng Ma, and Kai Chen. Decoy state quantum key distribution. *Physical review letters*, 94(23):230504, 2005.
[135] Jarrod R McClean, Jonathan Romero, Ryan Babbush, and Alán Aspuru-Guzik. The theory of variational hybrid quantum-classical algorithms. *New Journal of Physics*, 18(2):023023, 2016.

[136] Robin Milner. A theory of type polymorphism in programming. *Journal of Computer and System Sciences*, 17(3):348–375, 1978.

[137] Rajagopal Nagarajan and Simon Gay. Formal verification of quantum protocols. Available online as arXiv:quant-ph/0203086, 2002.

[138] Yunseong Nam, Neil J Ross, Yuan Su, Andrew M Childs, and Dmitri Maslov. Automated optimization of large quantum circuits with continuous parameters. *npj Quantum Information*, 4(1):1–12, 2018.

[139] Michael A. Nielsen and Isaac Chuang. *Quantum computation and quantum information*. Cambridge University Press, Cambridge, United Kingdom, 2002.

[140] Michael A. Nielsen and Isaac L. Chuang. *Quantum Computation and Quantum Information (10th Anniversary edition)*. Cambridge University Press, 2016.

[141] Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. *Isabelle/HOL: a proof assistant for higher-order logic*. Springer, 2002.

[142] Berhnard Ömer. *Structured Quantum Programming*. PhD thesis, TU Wien, 2003.

[143] Michele Pagani, Peter Selinger, and Benoît Valiron. Applying quantitative semantics to higher-order quantum computing. In *Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages*, POPL '14, page 647–658, New York, NY, USA, 2014. Association for Computing Machinery.

[144] Luca Paolini and Margherita Zorzi. qPCF: A language for quantum circuit computations. In T. V. Gopal, Gerhard Jäger, and Silvia Steila, editors, *Proceedings of the 14th Annual Conference on Theory and Applications of Models of Computation (TAMC'17)*, volume 10185 of *Lecture Notes in Computer Science*, pages 455–469, Bern, Switzerland, 2017.

[145] Christine Paulin-Mohring. Introduction to the calculus of inductive constructions. In *volume 55 of Studies in Logic (Mathematical logic and foundations)*. College Publications, 2015.

[146] Christine Paulin-Mohring. Introduction to the calculus of inductive constructions. In Bruno Woltzenlogel, Paleo and David Delahaye, editors, *All about Proofs, Proofs for All*, volume 55 of *Studies in Logic (Mathematical logic and foundations)*. College Publications, 2015.

[147] Jennifer Paykin. *Linear/non-Linear Types For Embedded Domain-Specific Languages*. PhD thesis, University of Pennsylvania, 2018.

[148] Jennifer Paykin, Robert Rand, and Steve Zdancewic. QWIRE: a core language for quantum circuits. In Giuseppe Castagna and Andrew D. Gordon, editors, *Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL'17)*, pages 846–858, Paris, France, 2017. ACM.

[149] Simon Perdrix. Quantum entanglement analysis based on abstract interpretation. In *International Static Analysis Symposium*, pages 270–282. Springer, 2008.
[135] Jarrod R McClean, Jonathan Romero, Ryan Babbush, and Alán Aspuru-Guzik. The theory of variational hybrid quantum-classical algorithms. *New Journal of Physics*, 18(2):023023, 2016.

[136] Robin Milner. A theory of type polymorphism in programming. *Journal of Computer and System Sciences*, 17(3):348–375, 1978.

[137] Rajagopal Nagarajan and Simon Gay. Formal verification of quantum protocols. Available online as arXiv:quant-ph/0203086, 2002.

[138] Yunseong Nam, Neil J Ross, Yuan Su, Andrew M Childs, and Dmitri Maslov. Automated optimization of large quantum circuits with continuous parameters. *npj Quantum Information*, 4(1):1–12, 2018.

[139] Michael A. Nielsen and Isaac Chuang. *Quantum computation and quantum information*. Cambridge University Press, Cambridge, United Kingdom, 2002.

[140] Michael A. Nielsen and Isaac L. Chuang. *Quantum Computation and Quantum Information (10th Anniversary edition)*. Cambridge University Press, 2016.

[141] Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. *Isabelle/HOL: a proof assistant for higher-order logic*. Springer, 2002.

[142] Berhnard Ömer. *Structured Quantum Programming*. PhD thesis, TU Wien, 2003.

[143] Michele Pagani, Peter Selinger, and Benoît Valiron. Applying quantitative semantics to higher-order quantum computing. In *Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages*, POPL '14, page 647–658, New York, NY, USA, 2014. Association for Computing Machinery.

[144] Luca Paolini and Margherita Zorzi. qPCF: A language for quantum circuit computations. In T. V. Gopal, Gerhard Jäger, and Silvia Steila, editors, *Proceedings of the 14th Annual Conference on Theory and Applications of Models of Computation (TAMC'17)*, volume 10185 of *Lecture Notes in Computer Science*, pages 455–469, Bern, Switzerland, 2017.

[145] Christine Paulin-Mohring. Introduction to the calculus of inductive constructions. In *volume 55 of Studies in Logic (Mathematical logic and foundations)*. College Publications, 2015.

[146] Christine Paulin-Mohring. Introduction to the calculus of inductive constructions. In Bruno Woltzenlogel, Paleo and David Delahaye, editors, *All about Proofs, Proofs for All*, volume 55 of *Studies in Logic (Mathematical logic and foundations)*. College Publications, 2015.

[147] Jennifer Paykin. *Linear/non-Linear Types For Embedded Domain-Specific Languages*. PhD thesis, University of Pennsylvania, 2018.

[148] Jennifer Paykin, Robert Rand, and Steve Zdancewic. QWIRE: a core language for quantum circuits. In Giuseppe Castagna and Andrew D. Gordon, editors, *Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL'17)*, pages 846–858, Paris, France, 2017. ACM.

[149] Simon Perdrix. Quantum entanglement analysis based on abstract interpretation. In *International Static Analysis Symposium*, pages 270–282. Springer, 2008.
[150] Benjamin C. Pierce. *Types and Programming Languages*. MIT Press, 2002.

[151] Amir Pnueli. The temporal logic of programs. In *18th Annual Symposium on Foundations of Computer Science (sfcs 1977)*, pages 46–57. iee, 1977.

[152] John Preskill. Quantum computing in the NISQ era and beyond. *Quantum*, 2:79, 2018.

[153] Qiskit Community. Qiskit: An open-source framework for quantum computing, March 2017. The official way to cite Qiskit is using the bibentry at https://github.com/Qiskit/qiskit/blob/master/Qiskit.bib.

[154] Quantum Computing Report. List of tools. Available online<fnref n="17" />, 2019.

[155] Robert Rand, Kesha Hietala, and Michael Hicks. Formal verification vs. quantum uncertainty. In *3rd Summit on Advances in Programming Languages (SNAPL 2019)*. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2019.

[156] Robert Rand, Jennifer Paykin, and Steve Zdancewic. QWIRE practice: Formal verification of quantum circuits in Coq. In Bob Coecke and Aleks Kissinger, editors, *Proceedings 14th International Conference on Quantum Physics and Logic (QPL 2017)*, volume 266 of *Electronic Proceedings in Theoretical Computer Science*, pages 119–132, Nijmegen, The Netherlands, 2017. EPTCS.

[157] Robert Raussendorf, Daniel E Browne, and Hans J Briegel. Measurement-based quantum computation on cluster states. *Physical review A*, 68(2):022312, 2003.

[158] John C Reynolds. Separation logic: A logic for shared mutable data structures. In *Proceedings 17th Annual IEEE Symposium on Logic in Computer Science*, pages 55–74. IEEE, 2002.

[159] Francisco Rios. *On a Categorically Sound Quantum Programming Language for Circuit Description*. PhD thesis, Dalhousie University, Halifax, Nova Scotia, Canada, August 2021.

[160] Francisco Rios and Peter Selinger. A categorical model for a quantum circuit description language. In Bob Coecke and Aleks Kissinger, editors, *Proceedings 14th International Conference on Quantum Physics and Logic (QPL 2017)*, volume 266 of *Electronic Proceedings in Theoretical Computer Science*, pages 164–178, Nijmegen, The Netherlands, 2018.

[161] Xavier Rival and Kwangkeun Yi. *Introduction to Static Analysis: An Abstract Interpretation Perspective*. The MIT Press, 2020.

[162] Neil J. Ross. *Algebraic and Logical Methods in Quantum Computation*. PhD thesis, Dalhousie University, 2015. Available as arxiv:1510.02198.

[163] Thomas Santoli and Christian Schaffner. Using Simon's algorithm to attack symmetric-key cryptographic primitives. *Quantum Inf. Comput.*, 17(1&2):65–78, 2017.

[164] Valerio Scarani, Helle Bechmann-Pasquinucci, Nicolas J Cerf, Miloslav Dušek, Norbert Lütkenhaus, and Momtchil Peev. The security of practical quantum key distribution. *Reviews of modern physics*, 81(3):1301, 2009.

<footnote n="17">¹⁷https://quantumcomputingreport.com/resources/tools/</footnote>
[150] Benjamin C. Pierce. *Types and Programming Languages*. MIT Press, 2002.

[151] Amir Pnueli. The temporal logic of programs. In *18th Annual Symposium on Foundations of Computer Science (sfcs 1977)*, pages 46–57. iee, 1977.

[152] John Preskill. Quantum computing in the NISQ era and beyond. *Quantum*, 2:79, 2018.

[153] Qiskit Community. Qiskit: An open-source framework for quantum computing, March 2017. The official way to cite Qiskit is using the bibentry at https://github.com/Qiskit/qiskit/blob/master/Qiskit.bib.

[154] Quantum Computing Report. List of tools. Available online<fnref n="17" />, 2019.

[155] Robert Rand, Kesha Hietala, and Michael Hicks. Formal verification vs. quantum uncertainty. In *3rd Summit on Advances in Programming Languages (SNAPL 2019)*. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2019.

[156] Robert Rand, Jennifer Paykin, and Steve Zdancewic. QWIRE practice: Formal verification of quantum circuits in Coq. In Bob Coecke and Aleks Kissinger, editors, *Proceedings 14th International Conference on Quantum Physics and Logic (QPL 2017)*, volume 266 of *Electronic Proceedings in Theoretical Computer Science*, pages 119–132, Nijmegen, The Netherlands, 2017. EPTCS.

[157] Robert Raussendorf, Daniel E Browne, and Hans J Briegel. Measurement-based quantum computation on cluster states. *Physical review A*, 68(2):022312, 2003.

[158] John C Reynolds. Separation logic: A logic for shared mutable data structures. In *Proceedings 17th Annual IEEE Symposium on Logic in Computer Science*, pages 55–74. IEEE, 2002.

[159] Francisco Rios. *On a Categorically Sound Quantum Programming Language for Circuit Description*. PhD thesis, Dalhousie University, Halifax, Nova Scotia, Canada, August 2021.

[160] Francisco Rios and Peter Selinger. A categorical model for a quantum circuit description language. In Bob Coecke and Aleks Kissinger, editors, *Proceedings 14th International Conference on Quantum Physics and Logic (QPL 2017)*, volume 266 of *Electronic Proceedings in Theoretical Computer Science*, pages 164–178, Nijmegen, The Netherlands, 2018.

[161] Xavier Rival and Kwangkeun Yi. *Introduction to Static Analysis: An Abstract Interpretation Perspective*. The MIT Press, 2020.

[162] Neil J. Ross. *Algebraic and Logical Methods in Quantum Computation*. PhD thesis, Dalhousie University, 2015. Available as arxiv:1510.02198.

[163] Thomas Santoli and Christian Schaffner. Using Simon's algorithm to attack symmetric-key cryptographic primitives. *Quantum Inf. Comput.*, 17(1&2):65–78, 2017.

[164] Valerio Scarani, Helle Bechmann-Pasquinucci, Nicolas J Cerf, Miloslav Dušek, Norbert Lütkenhaus, and Momtchil Peev. The security of practical quantum key distribution. *Reviews of modern physics*, 81(3):1301, 2009.

<footnote n="17">¹⁷https://quantumcomputingreport.com/resources/tools/</footnote>
[165] Artur Scherer, Benoît Valiron, Siun-Chuon Mau, Scott Alexander, Eric Van den Berg, and Thomas E Chapuran. Concrete resource analysis of the quantum linear-system algorithm used to compute the electromagnetic scattering cross section of a 2d target. *Quantum Information Processing*, 16(3):60, 2017.

[166] Maria Schuld. *Supervised Learning with Quantum Computers*. Springer, 2018.

[167] Dana Scott and Jacobus Willem de Bakker. A theory of programs. *Unpublished manuscript*, *IBM, Vienna*, 1969.

[168] Peter Selinger. Towards a quantum programming language. *Mathematical Structures in Computer Science*, 14(4):527–586, 2004.

[169] Peter Selinger. Generators and relations for $n$-qubit Clifford operators. *Logical Methods in Computer Science*, 11(2), Jun 2015.

[170] Peter Selinger and Benoît Valiron. A lambda calculus for quantum computation with classical control. In Paweł Urzyczyn, editor, *Typed Lambda Calculi and Applications*, pages 354–368, Berlin, Heidelberg, 2005. Springer Berlin Heidelberg.

[171] Peter Selinger and Benoît Valiron. A linear-non-linear model for a computational call-by-value lambda calculus (extended abstract). In Roberto M. Amadio, editor, *Proceedings of the 11th International Conference on Foundations of Software Science and Computational Structures (FOSSACS’08)*, volume 4962 of *Lecture Notes in Computer Science*, pages 81–96, Budapest, Hungary, 2008. Springer.

[172] Peter Selinger and Benoît Valiron. Quantum Lambda Calculus. In Simon J. Gay and Ian Mackie, editors, *Semantic Techniques in Quantum Computation*, pages 135–172. Cambridge University Press, Cambridge, November 2009.

[173] Yunong Shi, Runzhou Tao, Xupeng Li, Ali Javadi-Abhari, Andrew W Cross, Frederic T Chong, and Ronghui Gu. Certiq: A mostly-automated verification of a realistic quantum compiler. *arXiv preprint arXiv:1908.08963*, 2019.

[174] Peter W. Shor. Algorithms for quantum computation: Discrete log and factoring. In *Proceedings of the 35th Annual Symposium on Foundations of Computer Science (FOCS’94)*, pages 124–134, Santa Fe, New Mexico, US., 1994. IEEE, IEEE Computer Society Press.

[175] Peter W Shor. Scheme for reducing decoherence in quantum computer memory. *Physical review A*, 52(4):R2493, 1995.

[176] Daniel R Simon. On the power of quantum computation. *SIAM journal on computing*, 26(5):1474–1483, 1997.

[177] Kartik Singhal and John Reppy. Quantum hoare type theory: Extended abstract. In Benoît Valiron, Shane Mansfield, Pablo Arrighi, and Prakash Panangaden, editors, *Proceedings 17th International Conference on Quantum Physics and Logic, QPL 2020, Paris, France, June 2 - 6, 2020*, volume 340 of *EPTCS*, pages 291–302, 2020.

[178] Seyon Sivarajah, Silas Dilkes, Alexander Cowtan, Will Simmons, Alec Edgington, and Ross Duncan. $t|ket$: a retargetable compiler for NISQ devices. *Quantum Science and Technology*, 6(1):014003, 2020.
[165] Artur Scherer, Benoît Valiron, Siun-Chuon Mau, Scott Alexander, Eric Van den Berg, and Thomas E Chapuran. Concrete resource analysis of the quantum linear-system algorithm used to compute the electromagnetic scattering cross section of a 2d target. *Quantum Information Processing*, 16(3):60, 2017.

[166] Maria Schuld. *Supervised Learning with Quantum Computers*. Springer, 2018.

[167] Dana Scott and Jacobus Willem de Bakker. A theory of programs. *Unpublished manuscript*, *IBM, Vienna*, 1969.

[168] Peter Selinger. Towards a quantum programming language. *Mathematical Structures in Computer Science*, 14(4):527–586, 2004.

[169] Peter Selinger. Generators and relations for $n$-qubit Clifford operators. *Logical Methods in Computer Science*, 11(2), Jun 2015.

[170] Peter Selinger and Benoît Valiron. A lambda calculus for quantum computation with classical control. In Paweł Urzyczyn, editor, *Typed Lambda Calculi and Applications*, pages 354–368, Berlin, Heidelberg, 2005. Springer Berlin Heidelberg.

[171] Peter Selinger and Benoît Valiron. A linear-non-linear model for a computational call-by-value lambda calculus (extended abstract). In Roberto M. Amadio, editor, *Proceedings of the 11th International Conference on Foundations of Software Science and Computational Structures (FOSSACS’08)*, volume 4962 of *Lecture Notes in Computer Science*, pages 81–96, Budapest, Hungary, 2008. Springer.

[172] Peter Selinger and Benoît Valiron. Quantum Lambda Calculus. In Simon J. Gay and Ian Mackie, editors, *Semantic Techniques in Quantum Computation*, pages 135–172. Cambridge University Press, Cambridge, November 2009.

[173] Yunong Shi, Runzhou Tao, Xupeng Li, Ali Javadi-Abhari, Andrew W Cross, Frederic T Chong, and Ronghui Gu. Certiq: A mostly-automated verification of a realistic quantum compiler. *arXiv preprint arXiv:1908.08963*, 2019.

[174] Peter W. Shor. Algorithms for quantum computation: Discrete log and factoring. In *Proceedings of the 35th Annual Symposium on Foundations of Computer Science (FOCS’94)*, pages 124–134, Santa Fe, New Mexico, US., 1994. IEEE, IEEE Computer Society Press.

[175] Peter W Shor. Scheme for reducing decoherence in quantum computer memory. *Physical review A*, 52(4):R2493, 1995.

[176] Daniel R Simon. On the power of quantum computation. *SIAM journal on computing*, 26(5):1474–1483, 1997.

[177] Kartik Singhal and John Reppy. Quantum hoare type theory: Extended abstract. In Benoît Valiron, Shane Mansfield, Pablo Arrighi, and Prakash Panangaden, editors, *Proceedings 17th International Conference on Quantum Physics and Logic, QPL 2020, Paris, France, June 2 - 6, 2020*, volume 340 of *EPTCS*, pages 291–302, 2020.

[178] Seyon Sivarajah, Silas Dilkes, Alexander Cowtan, Will Simmons, Alec Edgington, and Ross Duncan. $t|ket$: a retargetable compiler for NISQ devices. *Quantum Science and Technology*, 6(1):014003, 2020.
[179] Sam Staton. Algebraic effects, linearity, and quantum programming languages. SIGPLAN Not., 50(1):395-406, January 2015.

[180] Damian S Steiger, Thomas Häner, and Matthias Troyer. ProjectQ: an open source software framework for quantum computing. Quantum, 2(49):10-22, 2018.

[181] Krysta M Svore, Alan Geller, Matthias Troyer, John Azariah, Christopher Granade, Bетina Heim, Vadym Kliuchnikov, Mariia Mykhailova, Andres Paz, and Martin Roetteler. Q#: Enabling scalable quantum computing and development with a high-level domain-specific language. Available online as arXiv:1803.00652, 2018.

[182] Nikhil Swamy, Cătălin Hrițcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, et al. Dependent types and multi-monadic effects in f. In Proceedings of the 43rd annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 256-270, 2016.

[183] Quingo Development Team. Quingo: A programming framework for heterogeneous quantum-classical computing with NISQ features. Draft available as arXiv:2009.01686, 2020.

[184] Dominique Unruh. Quantum Hoare logic with ghost variables. In 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1-13. IEEE, 2019.

[185] Dominique Unruh. Quantum relational Hoare logic. Proc. ACM Program. Lang., 3(POL):33:1-33:31, 2019.

[186] Benoît Valiron. Generating reversible circuits from higher-order functional programs. In Simon J. Devitt and Ivan Lanese, editors, Reversible Computation - 8th International Conference, RC 2016, Bologna, Italy, July 7-8, 2016, Proceedings, volume 9720 of Lecture Notes in Computer Science, pages 289-306. Springer, 2016.

[187] Wim Van Dam, Sean Hallgren, and Lawrence Ip. Quantum algorithms for some hidden shift problems. SIAM Journal on Computing, 36(3):763-778, 2006.

[188] André van Tonder. A lambda calculus for quantum computation. SIAM Journal on Computing, 33(5):1109-1135, 2004.

[189] Renaud Vilmart. A near-minimal axiomatisation of ZX-calculus for pure qubit quantum mechanics. In 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1-10, June 2019.

[190] Renaud Vilmart. The structure of sum-over-paths, its consequences, and completeness for Clifford, 2020. Available online as arXiv:2003.05678.

[191] Willem Visser, Corina S. Pasareanu, and Sarfraz Khurshid. Test input generation with Java PathFinder. In 2004 ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA '04. ACM, 2004.

[192] Chuan Wang, Fu-Guo Deng, Yan-Song Li, Xiao-Shu Liu, and Gui Lu Long. Quantum secure direct communication with high-dimension quantum superdense coding. Phys. Rev. A, 71:044305, Apr 2005.
[179] Sam Staton. Algebraic effects, linearity, and quantum programming languages. SIGPLAN Not., 50(1):395-406, January 2015.

[180] Damian S Steiger, Thomas Häner, and Matthias Troyer. ProjectQ: an open source software framework for quantum computing. Quantum, 2(49):10-22, 2018.

[181] Krysta M Svore, Alan Geller, Matthias Troyer, John Azariah, Christopher Granade, Bетina Heim, Vadym Kliuchnikov, Mariia Mykhailova, Andres Paz, and Martin Roetteler. Q#: Enabling scalable quantum computing and development with a high-level domain-specific language. Available online as arXiv:1803.00652, 2018.

[182] Nikhil Swamy, Cătălin Hriţcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, et al. Dependent types and multi-monadic effects in f. In Proceedings of the 43rd annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 256-270, 2016.

[183] Quingo Development Team. Quingo: A programming framework for heterogeneous quantum-classical computing with NISQ features. Draft available as arXiv:2009.01686, 2020.

[184] Dominique Unruh. Quantum Hoare logic with ghost variables. In 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1-13. IEEE, 2019.

[185] Dominique Unruh. Quantum relational Hoare logic. Proc. ACM Program. Lang., 3(POL):33:1-33:31, 2019.

[186] Benoît Valiron. Generating reversible circuits from higher-order functional programs. In Simon J. Devitt and Ivan Lanese, editors, Reversible Computation - 8th International Conference, RC 2016, Bologna, Italy, July 7-8, 2016, Proceedings, volume 9720 of Lecture Notes in Computer Science, pages 289-306. Springer, 2016.

[187] Wim Van Dam, Sean Hallgren, and Lawrence Ip. Quantum algorithms for some hidden shift problems. SIAM Journal on Computing, 36(3):763-778, 2006.

[188] André van Tonder. A lambda calculus for quantum computation. SIAM Journal on Computing, 33(5):1109-1135, 2004.

[189] Renaud Vilmart. A near-minimal axiomatisation of ZX-calculus for pure qubit quantum mechanics. In 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1-10, June 2019.

[190] Renaud Vilmart. The structure of sum-over-paths, its consequences, and completeness for Clifford, 2020. Available online as arXiv:2003.05678.

[191] Willem Visser, Corina S. Pasareanu, and Sarfraz Khurshid. Test input generation with Java PathFinder. In 2004 ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA '04. ACM, 2004.

[192] Chuan Wang, Fu-Guo Deng, Yan-Song Li, Xiao-Shu Liu, and Gui Lu Long. Quantum secure direct communication with high-dimension quantum superdense coding. Phys. Rev. A, 71:044305, Apr 2005.
[193] Dave Wecker and Krysta M Svore. LIQUi|>: A software design architecture and domain-specific language for quantum computing. Available online as arXiv:1402.4467, 2014.

[194] Mingsheng Ying. Floyd-Hoare logic for quantum programs. *ACM Transactions on Programming Languages and Systems (TOPLAS)*, 33(6):19:1–19:49, 2011.

[195] Mingsheng Ying. *Foundations of Quantum Programming*. Morgan Kaufmann, 2016.

[196] Mingsheng Ying and Yuan Feng. *Model Checking Quantum Systems: Principles and Algorithms*. Cambridge University Press, 2021.

[197] Mingsheng Ying, Yangjia Li, Nengkun Yu, and Yuan Feng. Model-checking linear-time properties of quantum systems. *ACM Transactions on Computational Logic*, 15(3):22:1–22:31, 2014.

[198] Mingsheng Ying, Shenggang Ying, and Xiaodi Wu. Invariants of quantum programs: characterisations and generation. In Giuseppe Castagna and Andrew D. Gordon, editors, *Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017*, pages 818–832. ACM, 2017.

[199] Nengkun Yu and Jens Palsberg. Quantum abstract interpretation. In *Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation*, pages 542–558, 2021.

[200] Shengyu Zhang. BQP-complete problems. In Grzegorz Rozenberg, Thomas Bäck, and Joost N. Kok, editors, *Handbook of Natural Computing*, pages 1545–1571. Springer, 2012.

[201] Li Zhou, Gilles Barthe, Justin Hsu, Mingsheng Ying, and Nengkun Yu. A quantum interpretation of bunched logic for quantum separation logic. In *2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)*, pages 1–14. IEEE, 2021.
[193] Dave Wecker and Krysta M Svore. LIQUi|>: A software design architecture and domain-specific language for quantum computing. Available online as arXiv:1402.4467, 2014.

[194] Mingsheng Ying. Floyd-Hoare logic for quantum programs. *ACM Transactions on Programming Languages and Systems (TOPLAS)*, 33(6):19:1–19:49, 2011.

[195] Mingsheng Ying. *Foundations of Quantum Programming*. Morgan Kaufmann, 2016.

[196] Mingsheng Ying and Yuan Feng. *Model Checking Quantum Systems: Principles and Algorithms*. Cambridge University Press, 2021.

[197] Mingsheng Ying, Yangjia Li, Nengkun Yu, and Yuan Feng. Model-checking linear-time properties of quantum systems. *ACM Transactions on Computational Logic*, 15(3):22:1–22:31, 2014.

[198] Mingsheng Ying, Shenggang Ying, and Xiaodi Wu. Invariants of quantum programs: characterisations and generation. In Giuseppe Castagna and Andrew D. Gordon, editors, *Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017*, pages 818–832. ACM, 2017.

[199] Nengkun Yu and Jens Palsberg. Quantum abstract interpretation. In *Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation*, pages 542–558, 2021.

[200] Shengyu Zhang. BQP-complete problems. In Grzegorz Rozenberg, Thomas Bäck, and Joost N. Kok, editors, *Handbook of Natural Computing*, pages 1545–1571. Springer, 2012.

[201] Li Zhou, Gilles Barthe, Justin Hsu, Mingsheng Ying, and Nengkun Yu. A quantum interpretation of bunched logic for quantum separation logic. In *2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)*, pages 1–14. IEEE, 2021.