Quantum PL & Verification Bibliography

Welcome to Quantum PL & Verification Bibliography maintained by Kartik Singhal. Browse without and with abstracts, bib entries. Please file issues/send PRs if you find any mistakes or missing entries. An alternate interface is available at quantumpl.github.io.

[1]	Samson Abramsky and Bob Coecke. A Categorical Semantics of Quantum Protocols. In Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, LICS '04, pages 415–425, Los Alamitos, CA, USA, July 2004. IEEE Computer Society. [ bib \| DOI \| arXiv \| Abstract ]
[2]	Samson Abramsky and Bob Coecke. Categorical Quantum Mechanics. In Kurt Engesser, Dov M. Gabbay, and Daniel Lehmann, editors, Handbook of Quantum Logic and Quantum Structures, pages 261–323. Elsevier, Amsterdam, November 2008. [ bib \| DOI \| arXiv \| Abstract ]
[3]	Thorsten Altenkirch and Jonathan Grattage. A Functional Quantum Programming Language. In Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science, LICS '05, pages 249–258, Los Alamitos, CA, USA, June 2005. IEEE Computer Society. [ bib \| DOI \| arXiv \| Abstract ]
[4]	Thorsten Altenkirch and Alexander S. Green. The Quantum IO Monad. In Gay and Mackie [55], pages 173–205. [ bib \| DOI \| .pdf \| Abstract ]
[5]	Matthew Amy. Formal Methods in Quantum Circuit Design. PhD thesis, University of Waterloo, Waterloo, Ontario, Canada, February 2019. [ bib \| http \| Abstract ]
[6]	Matthew Amy. Sized Types for Low-Level Quantum Metaprogramming. In Michael Kirkedal Thomsen and Mathias Soeken, editors, Reversible Computation (RC '19), volume 11497 of Lecture Notes in Computer Science, pages 87–107, Cham, May 2019. Springer International Publishing. [ bib \| DOI \| arXiv \| Abstract ]
[7]	Matthew Amy. Towards Large-Scale Functional Verification of Universal Quantum Circuits. In Peter Selinger and Giulio Chiribella, editors, Proceedings of the 15th International Conference on Quantum Physics and Logic (QPL), Halifax, Canada, June 3–7, 2018, volume 287 of Electronic Proceedings in Theoretical Computer Science, pages 1–21, Waterloo, NSW, Australia, January 2019. Open Publishing Association. [ bib \| DOI \| Abstract ]
[8]	Matthew Amy and Vlad Gheorghiu. staq – A full-stack quantum processing toolkit. Quantum Science and Technology, 5(3):034016, June 2020. [ bib \| DOI \| arXiv \| https \| Abstract ]
[9]	Ebrahim Ardeshir-Larijani, Simon J. Gay, and Rajagopal Nagarajan. Automated Equivalence Checking of Concurrent Quantum Systems. ACM Transactions on Computational Logic, 19(4):28, November 2018. [ bib \| DOI \| http \| Abstract ]
[10]	Miriam Backens. The ZX-calculus is complete for stabilizer quantum mechanics. New Journal of Physics, 16(9):093021, September 2014. [ bib \| DOI \| Abstract ]
[11]	Costin Bădescu and Prakash Panangaden. Quantum Alternation: Prospects and Problems. In Chris Heunen, Peter Selinger, and Jamie Vicary, editors, Proceedings of the 12th International Workshop on Quantum Physics and Logic (QPL), Oxford, U.K., July 15–17, 2015, volume 195 of Electronic Proceedings in Theoretical Computer Science, pages 33–42, Waterloo, NSW, Australia, November 2015. Open Publishing Association. [ bib \| DOI \| Abstract ]
[12]	John C. Baez and Mike Stay. Physics, Topology, Logic and Computation: A Rosetta Stone. In Bob Coecke, editor, New Structures for Physics, pages 95–172. Springer, Berlin, Heidelberg, July 2010. [ bib \| DOI \| arXiv \| Abstract ]
[13]	Stefano Bettelli, Tommaso Calarco, and Luciano Serafini. Toward an Architecture for Quantum Programming. European Physical Journal D: Atomic, Molecular, Optical and Plasma Physics, 25(2):181–200, August 2003. [ bib \| DOI \| arXiv \| Abstract ]
[14]	Benjamin Bichsel, Maximilian Baader, Timon Gehr, and Martin Vechev. Silq: A High-Level Quantum Language with Safe Uncomputation and Intuitive Semantics. In Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '20, pages 286–300, New York, NY, USA, June 2020. Association for Computing Machinery. [ bib \| DOI \| .pdf \| Abstract ]
[15]	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), Oxford, U.K., July 15–17, 2015, volume 195 of Electronic Proceedings in Theoretical Computer Science, pages 71–83, Waterloo, NSW, Australia, November 2015. Open Publishing Association. [ bib \| DOI \| Abstract ]
[16]	Anthony Bordg, Hanna Lachnitt, and Yijun He. Certified Quantum Computation in Isabelle/HOL. Journal of Automated Reasoning, 65(5):691–709, December 2020. [ bib \| DOI \| .html \| Abstract ]
[17]	Anthony Bordg, Hanna Lachnitt, and Yijun He. Isabelle Marries Dirac: a Library for Quantum Computation and Quantum Information. Archive of Formal Proofs, 2020, November 2020. [ bib \| .html \| Abstract ]
[18]	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. [ bib \| DOI \| arXiv \| Abstract ]
[19]	Kostia Chardonnet, Benoît Valiron, and Renaud Vilmart. Geometry of Interaction for ZX-Diagrams. In Filippo Bonchi and Simon J. Puglisi, editors, 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021), volume 202 of Leibniz International Proceedings in Informatics (LIPIcs), pages 30:1–30:16, Dagstuhl, Germany, August 2021. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. [ bib \| DOI \| https \| Abstract ]
[20]	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, ESOP 2021, volume 12648 of Lecture Notes in Computer Science, pages 148–177, Cham, March 2021. Springer International Publishing. [ bib \| DOI \| arXiv \| Abstract ]
[21]	Christophe Chareton, Sébastien Bardin, Dongho Lee, Benoît Valiron, Renaud Vilmart, and Zhaowei Xu. Formal Methods for Quantum Programs: A Survey, September 2021. To appear as Chapter “Formal methods for Quantum Algorithms” in “Handbook of Formal Analysis and Verification in Cryptography”, CRC. [ bib \| arXiv \| Abstract ]
[22]	Yu-Fang Chen, Kai-Min Chung, Ondřej Lengál, Jyun-Ao Lin, Wei-Lun Tsai, and Di-De Yen. An Automata-Based Framework for Verification and Bug Hunting in Quantum Circuits. Proceedings of the ACM on Programming Languages, 7(PLDI):156, June 2023. [ bib \| DOI \| Abstract ]
[23]	Frederic T. Chong, Diana Franklin, and Margaret Martonosi. Programming languages and compiler design for realistic quantum hardware. Nature, 549(7671):180–187, September 2017. Review Article. [ bib \| DOI \| Abstract ]
[24]	Vikraman Choudhury, Jacek Karwowski, and Amr Sabry. Symmetries in Reversible Programming: From Symmetric Rig Groupoids to Reversible Programming Languages. Proceedings of the ACM on Programming Languages, 6(POPL), January 2022. [ bib \| DOI \| https \| Abstract ]
[25]	Vikraman Choudhury, Amr Sabry, and Borislav Agapiev. Scheme Pearl: Quantum Continuations, September 2022. 2022 Workshop on Scheme and Functional Programming. [ bib \| .pdf \| Abstract ]
[26]	Cirq Developers. Cirq, July 2018. [ bib \| DOI \| https \| Abstract ]
[27]	Bob Coecke and Ross Duncan. Interacting Quantum Observables: Categorical Algebra and Diagrammatics. New Journal of Physics, 13(4):043016, April 2011. [ bib \| DOI \| Abstract ]
[28]	Bob Coecke and Aleks Kissinger. Picturing Quantum Processes: A First Course in Quantum Theory and Diagrammatic Reasoning. Cambridge University Press, Cambridge, March 2017. [ bib \| DOI \| Abstract ]
[29]	Andrea Colledan and Ugo Dal Lago. On Dynamic Lifting and Effect Typing in Circuit Description Languages (Extended Version), February 2022. [ bib \| arXiv \| Abstract ]
[30]	Andrew W. Cross, Lev S. Bishop, John A. Smolin, and Jay M. Gambetta. Open Quantum Assembly Language, July 2017. [ bib \| arXiv \| https \| Abstract ]
[31]	Andrew W. Cross, Ali Javadi-Abhari, Thomas Alexander, Niel de Beaudrap, Lev S. Bishop, Steven Heidel, Colm A. Ryan, Prasahnt Sivarajah, John Smolin, Jay M. Gambetta, and Blake R. Johnson. OpenQASM 3: A Broader and Deeper Quantum Assembly Language. ACM Transactions on Quantum Computing, 3(3):12, September 2022. [ bib \| DOI \| arXiv \| https \| Abstract ]
[32]	Ugo Dal Lago, Claudia Faggian, Benoît Valiron, and Akira Yoshimizu. The Geometry of Parallelism: Classical, Probabilistic, and Quantum Effects. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL '17, pages 833–845, New York, NY, USA, January 2017. Association for Computing Machinery. [ bib \| DOI \| arXiv \| Abstract ]
[33]	Liliane-Joy Dandy, Emmanuel Jeandel, and Vladimir Zamdzhiev. Qimaera: Type-safe (Variational) Quantum Programming in Idris, November 2021. [ bib \| arXiv \| https \| Abstract ]
[34]	Vincent Danos, Elham Kashefi, and Prakash Panangaden. The Measurement Calculus. Journal of the ACM, 54(2):8, April 2007. [ bib \| DOI \| .pdf \| Abstract ]
[35]	Vincent Danos, Elham Kashefi, Prakash Panangaden, and Simon Perdrix. Extended Measurement Calculus. In Gay and Mackie [55], pages 235–310. [ bib \| DOI \| Abstract ]
[36]	Ellie D'Hondt and Prakash Panangaden. Quantum Weakest Preconditions. Mathematical Structures in Computer Science, 16(3):429–451, June 2006. [ bib \| DOI \| .pdf \| Abstract ]
[37]	Alejandro Díaz-Caro. A Lambda Calculus for Density Matrices with Classical and Probabilistic Controls. In Bor-Yuh Evan Chang, editor, Programming Languages and Systems (APLAS 2017), volume 10695 of Lecture Notes in Computer Science, pages 448–467, Cham, November 2017. Springer International Publishing. [ bib \| DOI \| Abstract ]
[38]	Alejandro Díaz-Caro. A Quick Overview on the Quantum Control Approach to the Lambda Calculus. In Mauricio Ayala-Rincon and Eduardo Bonelli, editors, Proceedings of the 16th Workshop on Logical and Semantic Frameworks with Applications (LSFA), Buenos Aires, Argentina (Online), Juky 23–24, 2021, volume 357 of Electronic Proceedings in Theoretical Computer Science, pages 1–17, Waterloo, NSW, Australia, April 2022. Open Publishing Association. [ bib \| DOI \| Abstract ]
[39]	Alejandro Díaz-Caro, Pablo Arrighi, Manuel Gadella, and Jonathan Grattage. Measurements and Confluence in Quantum Lambda Calculi With Explicit Qubits. In Proceedings of the Joint 5th International Workshop on Quantum Physics and Logic and 4th Workshop on Developments in Computational Models (QPL/DCM 2008), volume 270/1 of Electronic Notes in Theoretical Computer Science, pages 59–74. Elsevier, February 2011. [ bib \| DOI \| Abstract ]
[40]	Alejandro Díaz-Caro and Gilles Dowek. Typing Quantum Superpositions and Measurement. In Carlos Martín-Vide, Roman Neruda, and Miguel A. Vega-Rodríguez, editors, Theory and Practice of Natural Computing (TPNC 2017), volume 10687 of Lecture Notes in Computer Science, pages 281–293, Cham, November 2017. Springer International Publishing. [ bib \| DOI \| Abstract ]
[41]	Alejandro Díaz-Caro and Gilles Dowek. A New Connective in Natural Deduction, and Its Application to Quantum Computing. In Antonio Cerone and Peter Csaba Ölveczky, editors, Theoretical Aspects of Computing – ICTAC 2021, volume 12819 of Lecture Notes in Computer Science, pages 175–193, Cham, August 2021. Springer International Publishing. [ bib \| DOI \| arXiv \| Abstract ]
[42]	Alejandro Díaz-Caro, Gilles Dowek, and Juan Pablo Rinaldi. Two linearities for quantum computing in the lambda calculus. Biosystems, 186:104012, December 2019. Selected papers from the International Conference on the Theory and Practice of Natural Computing (TPNC) 2017. [ bib \| DOI \| arXiv \| Abstract ]
[43]	Alejandro Díaz-Caro, Mauricio Guillermo, Alexandre Miquel, and Benoît Valiron. Realizability in the Unitary Sphere. In Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '19, page 56, Los Alamitos, CA, USA, June 2019. IEEE Computer Society. [ bib \| DOI \| arXiv \| Abstract ]
[44]	Alejandro Díaz-Caro and Octavio Malherbe. Quantum Control in the Unitary Sphere: Lambda-S1 and its Categorical Model. Logical Methods in Computer Science, 18(3):32, September 2022. [ bib \| DOI \| Abstract ]
[45]	Mnacho Echenim. Quantum projective measurements and the CHSH inequality. Archive of Formal Proofs, 2021, March 2021. [ bib \| .html \| Abstract ]
[46]	Mnacho Echenim and Mehdi Mhalla. Quantum projective measurements and the CHSH inequality in Isabelle/HOL, March 2021. [ bib \| arXiv \| Abstract ]
[47]	Yuan Feng, Sanjiang Li, and Mingsheng Ying. Verification of Distributed Quantum Programs. ACM Transactions on Computational Logic, 23(3):19, July 2022. [ bib \| DOI \| arXiv \| Abstract ]
[48]	Yuan Feng and Mingsheng Ying. Quantum Hoare Logic with Classical Variables. ACM Transactions on Quantum Computing, 2(4):16, December 2021. [ bib \| DOI \| arXiv \| Abstract ]
[49]	Peng Fu, Kohei Kishida, Neil J. Ross, and Peter Selinger. A Tutorial Introduction to Quantum Circuit Programming in Dependently Typed Proto-Quipper. In Ivan Lanese and Mariusz Rawski, editors, Reversible Computation (RC '20), volume 12227 of Lecture Notes in Computer Science, pages 153–168, Cham, July 2020. Springer International Publishing. [ bib \| DOI \| arXiv \| Abstract ]
[50]	Peng Fu, Kohei Kishida, Neil J. Ross, and Peter Selinger. A biset-enriched categorical model for Proto-Quipper with dynamic lifting. In Proceedings of the 19th International Conference on Quantum Physics and Logic (QPL), Oxford, U.K., June 27–July 1, 2022. Open Publishing Association, April 2022. To appear. [ bib \| arXiv \| Abstract ]
[51]	Peng Fu, Kohei Kishida, Neil J. Ross, and Peter Selinger. Proto-Quipper with Dynamic Lifting. Proceedings of the ACM on Programming Languages, 7(POPL):11, January 2023. [ bib \| DOI \| arXiv \| https \| Abstract ]
[52]	Peng Fu, Kohei Kishida, and Peter Selinger. Linear Dependent Type Theory for Quantum Programming Languages: Extended Abstract. In Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '20, pages 440–453, New York, NY, USA, July 2020. Association for Computing Machinery. [ bib \| DOI \| Abstract ]
[53]	Peng Fu, Kohei Kishida, and Peter Selinger. Linear Dependent Type Theory for Quantum Programming Languages. Logical Methods in Computer Science, 18(3):28, September 2022. [ bib \| DOI \| Abstract ]
[54]	Simon J. Gay. Quantum Programming Languages: Survey and Bibliography. Mathematical Structures in Computer Science, 16(4):581–600, August 2006. [ bib \| DOI \| http \| Abstract ]
[55]	Simon J. Gay and Ian Mackie, editors. Semantic Techniques in Quantum Computation. Cambridge University Press, Cambridge, November 2009. [ bib \| DOI \| Abstract ]
[56]	Simon J. Gay and Rajagopal Nagarajan. Communicating Quantum Processes. In Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '05, pages 145–157, New York, NY, USA, January 2005. Association for Computing Machinery. [ bib \| DOI \| arXiv \| .pdf \| Abstract ]
[57]	Simon J. Gay, Rajagopal Nagarajan, and Nikolaos Papanikolaou. QMC: A Model Checker for Quantum Systems. In Aarti Gupta and Sharad Malik, editors, Computer Aided Verification (CAV '08), volume 5123 of Lecture Notes in Computer Science, pages 543–547, Berlin, Heidelberg, July 2008. Springer. [ bib \| DOI \| arXiv \| Abstract ]
[58]	Vlad Gheorghiu. Quantum++: A modern C++ quantum computing library. PLoS ONE, 13(12):e0208073, December 2018. [ bib \| DOI \| https \| Abstract ]
[59]	Jonathan Grattage. An Overview of QML With a Concrete Implementation in Haskell. In Proceedings of the Joint 5th International Workshop on Quantum Physics and Logic and 4th Workshop on Developments in Computational Models (QPL/DCM 2008), volume 270/1 of Electronic Notes in Theoretical Computer Science, pages 165–174. Elsevier, February 2011. [ bib \| DOI \| arXiv \| Abstract ]
[60]	Alexander S. Green. Towards a Formally Verified Functional Quantum Programming Language. PhD thesis, University of Nottingham, July 2010. [ bib \| http \| Abstract ]
[61]	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, Reversible Computation (RC '13), volume 7948 of Lecture Notes in Computer Science, pages 110–124, Berlin, Heidelberg, July 2013. Springer. [ bib \| DOI \| arXiv \| Abstract ]
[62]	Alexander S. Green, Peter LeFanu Lumsdaine, Neil J. Ross, Peter Selinger, and Benoît Valiron. Quipper: A Scalable Quantum Programming Language. In Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '13, pages 333–342, New York, NY, USA, June 2013. Association for Computing Machinery. [ bib \| DOI \| arXiv \| Abstract ]
[63]	Thomas Häner, Vadym Kliuchnikov, Martin Roetteler, Mathias Soeken, and Alexander Vaschillo. QParallel: Explicit Parallelism for Programming Quantum Computers, October 2022. [ bib \| arXiv \| Abstract ]
[64]	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, February 2017. Eighth Games for Logic and Programming Languages Workshop (GaLoP). [ bib \| DOI \| arXiv \| Abstract ]
[65]	Bettina Heim. Development of Quantum Applications. PhD thesis, ETH Zurich, Zurich, December 2020. [ bib \| DOI \| Abstract ]
[66]	Bettina Heim, Mathias Soeken, Sarah Marshall, Christopher E. Granade, Martin Roetteler, Alan Geller, Matthias Troyer, and Krysta M. Svore. Quantum Programming Languages. Nature Reviews Physics, 2(12):709–722, December 2020. [ bib \| DOI \| https \| Abstract ]
[67]	Chris Heunen and Robin Kaarsgaard. Quantum Information Effects. Proceedings of the ACM on Programming Languages, 6(POPL):2, January 2022. [ bib \| DOI \| https \| Abstract ]
[68]	Chris Heunen and Jamie Vicary. Categories for Quantum Theory: An Introduction. Oxford University Press, Oxford, November 2019. [ bib \| DOI \| Abstract ]
[69]	Kesha Hietala. A Verified Software Toolchain For Quantum Programming. PhD thesis, University of Maryland, College Park, MD, USA, July 2022. [ bib \| DOI \| Abstract ]
[70]	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), volume 193 of Leibniz International Proceedings in Informatics (LIPIcs), pages 21:1–21:19, Dagstuhl, Germany, June 2021. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. [ bib \| DOI \| https \| Abstract ]
[71]	Kesha Hietala, Robert Rand, Shih-Han Hung, Xiaodi Wu, and Michael Hicks. A Verified Optimizer for Quantum Circuits. Proceedings of the ACM on Programming Languages, 5(POPL):37, January 2021. [ bib \| DOI \| arXiv \| https \| Abstract ]
[72]	Kentaro Honda. Analysis of Quantum Entanglement in Quantum Programs using Stabilizer Formalism. In Chris Heunen, Peter Selinger, and Jamie Vicary, editors, Proceedings of the 12th International Workshop on Quantum Physics and Logic (QPL), Oxford, U.K., July 15–17, 2015, volume 195 of Electronic Proceedings in Theoretical Computer Science, pages 262–272, Waterloo, NSW, Australia, November 2015. Open Publishing Association. [ bib \| DOI \| Abstract ]
[73]	Yipeng Huang and Margaret Martonosi. QDB: From Quantum Algorithms Towards Correct Quantum Programs. In Titus Barik, Joshua Sunshine, and Sarah Chasins, editors, 9th Workshop on Evaluation and Usability of Programming Languages and Tools (PLATEAU 2018), volume 67 of OpenAccess Series in Informatics (OASIcs), pages 4:1–4:14, Dagstuhl, Germany, January 2019. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. [ bib \| DOI \| Abstract ]
[74]	Mathieu Huot and Sam Staton. Quantum channels as a categorical completion. In Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '19, page 35, Los Alamitos, CA, USA, June 2019. IEEE Computer Society. [ bib \| DOI \| arXiv \| Abstract ]
[75]	Mathieu Huot and Sam Staton. Universal Properties in Quantum Theory. In Peter Selinger and Giulio Chiribella, editors, Proceedings of the 15th International Conference on Quantum Physics and Logic (QPL), Halifax, Canada, June 3–7, 2018, volume 287 of Electronic Proceedings in Theoretical Computer Science, pages 213–223, Waterloo, NSW, Australia, January 2019. Open Publishing Association. [ bib \| DOI \| Abstract ]
[76]	David Ittah, Thomas Häner, Vadym Kliuchnikov, and Torsten Hoefler. QIRO: A Static Single Assignment-Based Quantum Program Representation for Optimization. ACM Transactions on Quantum Computing, 3(3):14, July 2022. [ bib \| DOI \| arXiv \| Abstract ]
[77]	Ali Javadi-Abhari, Arvin Faruque, Mohammad Javad Dousti, Lukas Svec, Oana Catu, Amlan Chakrabarti, Chen-Fu Chiang, Seth Vanderwilt, John Black, Frederic T. Chong, Margaret Martonosi, Martin Suchara, Ken Brown, Massoud Pedram, and Todd Brun. Scaffold: Quantum Programming Language. Technical Report TR-934-12, Princeton University, June 2012. [ bib \| https \| Abstract ]
[78]	Ali Javadi-Abhari, 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, June 2015. [ bib \| DOI \| arXiv \| Abstract ]
[79]	Xiaodong Jia, Andre Kornell, Bert Lindenhovius, Michael Mislove, and Vladimir Zamdzhiev. Semantics for Variational Quantum Programming. Proceedings of the ACM on Programming Languages, 6(POPL):26, January 2022. [ bib \| DOI \| arXiv \| Abstract ]
[80]	Philippe Jorrand and Simon Perdrix. Abstract Interpretation Techniques for Quantum Computation. In Gay and Mackie [55], pages 206–234. [ bib \| DOI \| Abstract ]
[81]	Chan Gu Kang and Hakjoo Oh. Modular Component-Based Quantum Circuit Synthesis. Proceedings of the ACM on Programming Languages, 7(OOPSLA1):87, April 2023. [ bib \| DOI \| https \| Abstract ]
[82]	Emanuel Knill. Conventions for Quantum Pseudocode. Technical Report LA-UR-96-2724, Los Alamos National Laboratory, June 1996. [ bib \| DOI \| Abstract ]
[83]	Martin Kong. On the Impact of Affine Loop Transformations in Qubit Allocation. ACM Transactions on Quantum Computing, 2(3):9, September 2021. [ bib \| DOI \| Abstract ]
[84]	Andre Kornell, Bert Lindenhovius, and Michael Mislove. Quantum CPOs. In Benoît Valiron, Shane Mansfield, Pablo Arrighi, and Prakash Panangaden, editors, Proceedings of the 17th International Conference on Quantum Physics and Logic (QPL), Paris, France, June 2–6, 2020, volume 340 of Electronic Proceedings in Theoretical Computer Science, pages 174–187, Waterloo, NSW, Australia, September 2021. Open Publishing Association. [ bib \| DOI \| Abstract ]
[85]	Ryan LaRose. Overview and Comparison of Gate Level Quantum Software Platforms. Quantum, 3:130, March 2019. [ bib \| DOI \| Abstract ]
[86]	Ryan LaRose, Andrea Mari, Sarah Kaiser, Peter J. Karalekas, Andre A. Alves, Piotr Czarnik, Mohamed El Mandouh, Max H. Gordon, Yousef Hindy, Aaron Robertson, Purva Thakre, Misty Wahl, Danny Samuel, Rahul Mistri, Maxime Tremblay, Nick Gardner, Nathaniel T. Stemen, Nathan Shammah, and William J. Zeng. Mitiq: A software package for error mitigation on noisy quantum computers. Quantum, 6:774, August 2022. [ bib \| DOI \| https \| Abstract ]
[87]	Xuan-Bach Le, Shang-Wei Lin, Jun Sun, and David Sanan. A Quantum Interpretation of Separating Conjunction for Local Reasoning of Quantum Programs Based on Separation Logic. Proceedings of the ACM on Programming Languages, 6(POPL):36, January 2022. [ bib \| DOI \| Abstract ]
[88]	Dongho Lee, Valentin Perrelle, Benoît Valiron, and Zhaowei Xu. Concrete Categorical Model of a Quantum Circuit Description Language with Measurement. In Mikołaj Bojańczy and Chandra Chekuri, editors, 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021), volume 213 of Leibniz International Proceedings in Informatics (LIPIcs), pages 51:1–51:20, Dagstuhl, Germany, November 2021. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. [ bib \| DOI \| Abstract ]
[89]	Marco Lewis, Sadegh Soudjani, and Paolo Zuliani. Formal Verification of Quantum Programs: Theory, Tools and Challenges, October 2021. [ bib \| arXiv \| Abstract ]
[90]	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):150, November 2020. [ bib \| DOI \| Abstract ]
[91]	Liyi Li, Finn Voichick, Kesha Hietala, Yuxiang Peng, Xiaodi Wu, and Michael Hicks. Verified Compilation of Quantum Oracles. Proceedings of the ACM on Programming Languages, 6(OOPSLA2):146, October 2022. [ bib \| DOI \| arXiv \| https \| Abstract ]
[92]	Yangjia Li and Dominique Unruh. Quantum Relational Hoare Logic with Expectations. In Nikhil Bansal, Emanuela Merelli, and James Worrell, editors, 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021), volume 198 of Leibniz International Proceedings in Informatics (LIPIcs), pages 136:1–136:20, Dagstuhl, Germany, July 2021. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. [ bib \| DOI \| Abstract ]
[93]	Yangjia Li and Mingsheng Ying. Algorithmic Analysis of Termination Problems for Quantum Programs. Proceedings of the ACM on Programming Languages, 2(POPL):35, December 2017. [ bib \| DOI \| Abstract ]
[94]	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, LICS '18, pages 659–668, New York, NY, USA, July 2018. Association for Computing Machinery. [ bib \| DOI \| arXiv \| Abstract ]
[95]	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 (CAV '19), volume 11562 of Lecture Notes in Computer Science, pages 187–207, Cham, July 2019. Springer International Publishing. [ bib \| DOI \| Abstract ]
[96]	Junyi Liu, Bohua Zhan, Shuling Wang, Shenggang Ying, Tao Liu, Yangjia Li, Mingsheng Ying, and Naijun Zhan. Quantum Hoare Logic. Archive of Formal Proofs, 2019, March 2019. [ bib \| .html \| Abstract ]
[97]	Mohamed Yousri Mahmoud and Amy P. Felty. Formalization of Metatheory of the Quipper Quantum Programming Language in a Linear Logic. Journal of Automated Reasoning, 63(4):967–1002, June 2019. [ bib \| DOI \| arXiv \| Abstract ]
[98]	Alexander McCaskey and Thien Nguyen. A MLIR Dialect for Quantum Assembly Languages. In 2021 IEEE International Conference on Quantum Computing and Engineering (QCE), pages 255–264, Los Alamitos, CA, USA, oct 2021. IEEE Computer Society. [ bib \| DOI \| arXiv \| Abstract ]
[99]	Alexander McCaskey, Thien Nguyen, Anthony Santana, Daniel Claudino, Tyler Kharazi, and Hal Finkel. Extending C++ for Heterogeneous Quantum-Classical Computing. ACM Transactions on Quantum Computing, 2(2):6, June 2021. [ bib \| DOI \| arXiv \| Abstract ]
[100]	Giulia Meuli, Mathias Soeken, Martin Roetteler, and Thomas Häner. Enabling Accuracy-Aware Quantum Compilers Using Symbolic Resource Estimation. Proceedings of the ACM on Programming Languages, 4(OOPSLA):130, November 2020. [ bib \| DOI \| Abstract ]
[101]	Microsoft. Q# Language Specification, September 2020. [ bib \| https \| Abstract ]
[102]	Michele Mosca, Martin Roetteler, and Peter Selinger. Quantum Programming Languages (Dagstuhl Seminar 18381). Dagstuhl Reports, 8(9):112–132, March 2019. [ bib \| DOI \| https \| Abstract ]
[103]	Thien Nguyen and Alexander McCaskey. Retargetable Optimizing Compilers for Quantum Accelerators via a Multilevel Intermediate Representation. IEEE Micro, 42(5):17–33, September 2022. [ bib \| DOI \| arXiv \| Abstract ]
[104]	Michael A. Nielsen and Isaac L. Chuang. Quantum Computation and Quantum Information: 10th Anniversary Edition. Cambridge University Press, Cambridge, December 2010. [ bib \| DOI \| Abstract ]
[105]	Bernhard Ömer. Structured Quantum Programming. PhD thesis, Vienna University of Technology, May 2003. [ bib \| .pdf ]
[106]	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, pages 647–658, New York, NY, USA, January 2014. Association for Computing Machinery. [ bib \| DOI \| arXiv \| Abstract ]
[107]	Matteo Paltenghi and Michael Pradel. Bugs in Quantum Computing Platforms: An Empirical Study. Proceedings of the ACM on Programming Languages, 6(OOPSLA1):86, April 2022. [ bib \| DOI \| Abstract ]
[108]	Luca Paolini, Mauro Piccolo, and Margherita Zorzi. QPCF: Higher-Order Languages and Quantum Circuits. Journal of Automated Reasoning, 63(4):941–966, March 2019. [ bib \| DOI \| arXiv \| Abstract ]
[109]	Luca Paolini, Luca Roversi, and Margherita Zorzi. Quantum Programming Made Easy. In Thomas Ehrhard, Maribel Fernández, Valeria de Paiva, and Lorenzo Tortora de Falco, editors, Proceedings Joint International Workshop on Linearity & Trends in Linear Logic and Applications (Linearity-TLLA '18), Oxford, UK, 7–8 July 2018, volume 292 of Electronic Proceedings in Theoretical Computer Science, pages 133–147. Open Publishing Association, April 2019. [ bib \| DOI \| Abstract ]
[110]	Luca Paolini and Margherita Zorzi. qPCF: A Language for Quantum Circuit Computations. In Theory and Applications of Models of Computation (TAMC '17), volume 10185 of Lecture Notes in Computer Science, pages 455–469, Cham, April 2017. Springer International Publishing. [ bib \| DOI \| Abstract ]
[111]	Anouk Paradis, Benjamin Bichsel, Samuel Steffen, and Martin Vechev. Unqomp: Synthesizing Uncomputation in Quantum Circuits. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI '21, pages 222–236, New York, NY, USA, June 2021. Association for Computing Machinery. [ bib \| DOI \| Abstract ]
[112]	Jennifer Paykin. Linear/Non-Linear Types for Embedded Domain-Specific Languages. PhD thesis, University of Pennsylvania, Philadelphia, PA, USA, August 2018. Publicly Accessible Penn Dissertations. 2752. [ bib \| https \| Abstract ]
[113]	Jennifer Paykin, Robert Rand, and Steve Zdancewic. QWIRE: A Core Language for Quantum Circuits. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL '17, pages 846–858, New York, NY, USA, January 2017. Association for Computing Machinery. [ bib \| DOI \| .pdf \| Abstract ]
[114]	Jennifer Paykin and Steve Zdancewic. A HoTT Quantum Equational Theory (Extended Version), April 2019. QPL '19. [ bib \| arXiv \| Abstract ]
[115]	Romain Péchoux, Simon Perdrix, Mathys Rennela, and Vladimir Zamdzhiev. Quantum Programming with Inductive Datatypes: Causality and Affine Type Theory. In Jean Goubault-Larrecq and Barbara König, editors, Foundations of Software Science and Computation Structures, FoSSaCS 2020, volume 12077 of Lecture Notes in Computer Science, pages 562–581, Cham, April 2020. Springer International Publishing. [ bib \| DOI \| Abstract ]
[116]	Anurudh Peduri, Siddharth Bhat, and Tobias Grosser. QSSA: An SSA-Based IR for Quantum Computing. In Proceedings of the 31st ACM SIGPLAN International Conference on Compiler Construction, pages 2–14, New York, NY, USA, March 2022. Association for Computing Machinery. [ bib \| DOI \| arXiv \| Abstract ]
[117]	Yuxiang Peng, Kesha Hietala, Runzhou Tao, Liyi Li, Robert Rand, Michael Hicks, and Xiaodi Wu. A Formally Certified End-to-End Implementation of Shor's Factorization Algorithm, April 2022. [ bib \| arXiv \| https \| Abstract ]
[118]	Yuxiang Peng, Mingsheng Ying, and Xiaodi Wu. Algebraic Reasoning of Quantum Programs via Non-Idempotent Kleene Algebra. In Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI '22, pages 657–670, New York, NY, USA, June 2022. Association for Computing Machinery. [ bib \| DOI \| arXiv \| Abstract ]
[119]	QIR Alliance. QIR Specification, November 2021. Also see https://qir-alliance.org. [ bib \| https \| Abstract ]
[120]	Qiskit Community. Qiskit: An Open-Source Framework for Quantum Computing, March 2017. [ bib \| DOI \| https \| Abstract ]
[121]	Quingo Development Team. Quingo: A Programming Framework for Heterogeneous Quantum-Classical Computing with NISQ Features. ACM Transactions on Quantum Computing, 2(4):19, December 2021. [ bib \| DOI \| https \| Abstract ]
[122]	Robert Rand. Verification Logics for Quantum Programs, March 2016. Submitted as a qualifying examination (WPE-II) for the PhD program at the University of Pennsylvania. [ bib \| arXiv \| Abstract ]
[123]	Robert Rand. Formally Verified Quantum Programming. PhD thesis, University of Pennsylvania, Philadelphia, PA, USA, November 2018. Publicly Accessible Penn Dissertations. 3175. [ bib \| https \| Abstract ]
[124]	Robert Rand, Kesha Hietala, and Michael Hicks. Formal Verification vs. Quantum Uncertainty. In Benjamin S. Lerner, Rastislav Bodík, and Shriram Krishnamurthi, editors, 3rd Summit on Advances in Programming Languages (SNAPL 2019), volume 136 of Leibniz International Proceedings in Informatics (LIPIcs), pages 12:1–12:11, Dagstuhl, Germany, July 2019. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. [ bib \| DOI \| Abstract ]
[125]	Robert Rand, Jennifer Paykin, Dongho Lee, and Steve Zdancewic. ReQWIRE: Reasoning about Reversible Quantum Circuits. In Peter Selinger and Giulio Chiribella, editors, Proceedings of the 15th International Conference on Quantum Physics and Logic (QPL), Halifax, Canada, June 3–7, 2018, volume 287 of Electronic Proceedings in Theoretical Computer Science, pages 299–312, Waterloo, NSW, Australia, January 2019. Open Publishing Association. [ bib \| DOI \| Abstract ]
[126]	Robert Rand, Jennifer Paykin, and Steve Zdancewic. Phantom Types for Quantum Programs, January 2018. Talk at The Fourth International Workshop on Coq for Programming Languages (CoqPL '18). [ bib \| https \| Abstract ]
[127]	Robert Rand, Jennifer Paykin, and Steve Zdancewic. QWIRE Practice: Formal Verification of Quantum Circuits in Coq. In Bob Coecke and Aleks Kissinger, editors, Proceedings of the 14th International Conference on Quantum Physics and Logic (QPL), Nijmegen, the Netherlands, July 3–7, 2017, volume 266 of Electronic Proceedings in Theoretical Computer Science, pages 119–132, Waterloo, NSW, Australia, February 2018. Open Publishing Association. [ bib \| DOI \| Abstract ]
[128]	Robert Rand, Aarthi Sundaram, Kartik Singhal, and Brad Lackey. Gottesman Types for Quantum Programs. In Benoît Valiron, Shane Mansfield, Pablo Arrighi, and Prakash Panangaden, editors, Proceedings of the 17th International Conference on Quantum Physics and Logic (QPL), Paris, France, June 2–6, 2020, volume 340 of Electronic Proceedings in Theoretical Computer Science, pages 279–290, Waterloo, NSW, Australia, September 2021. Open Publishing Association. [ bib \| DOI \| https \| Abstract ]
[129]	Mathys Rennela and Sam Staton. Classical Control and Quantum Circuits in Enriched Category Theory. In The Thirty-Third Conference on the Mathematical Foundations of Programming Semantics (MFPS XXXIII), volume 336 of Electronic Notes in Theoretical Computer Science, pages 257–279. Elsevier, April 2018. [ bib \| DOI \| Abstract ]
[130]	Mathys Rennela and Sam Staton. Classical Control, Quantum Circuits and Linear Logic in Enriched Category Theory. Logical Methods in Computer Science, 16(1):30, March 2020. [ bib \| DOI \| Abstract ]
[131]	Francisco Rios. On a Categorically Sound Quantum Programming Language for Circuit Description. PhD thesis, Dalhousie University, Halifax, Nova Scotia, Canada, August 2021. [ bib \| https \| Abstract ]
[132]	Francisco Rios and Peter Selinger. A Categorical Model for a Quantum Circuit Description Language (Extended Abstract). In Bob Coecke and Aleks Kissinger, editors, Proceedings of the 14th International Conference on Quantum Physics and Logic (QPL), Nijmegen, the Netherlands, July 3–7, 2017, volume 266 of Electronic Proceedings in Theoretical Computer Science, pages 164–178, Waterloo, NSW, Australia, February 2018. Open Publishing Association. [ bib \| DOI \| Abstract ]
[133]	Neil J. Ross. Algebraic and Logical Methods in Quantum Computation. PhD thesis, Dalhousie University, Halifax, Nova Scotia, Canada, August 2015. [ bib \| arXiv \| Abstract ]
[134]	Roland Rüdiger. Quantum Programming Languages: An Introductory Overview. The Computer Journal, 50(2):134–150, March 2007. [ bib \| DOI \| Abstract ]
[135]	Amr Sabry, Benoît Valiron, and Juliana Kaizer Vizzotto. From Symmetric Pattern-Matching to Quantum Control. In Christel Baier and Ugo Dal Lago, editors, Foundations of Software Science and Computation Structures, FoSSaCS 2018, volume 10803 of Lecture Notes in Computer Science, pages 348–364, Cham, April 2018. Springer International Publishing. [ bib \| DOI \| arXiv \| Abstract ]
[136]	Peter Selinger. A Brief Survey of Quantum Programming Languages. In Yukiyoshi Kameyama and Peter J. Stuckey, editors, Proceedings of the 7th International Symposium on Functional and Logic Programming, volume 2998 of Lecture Notes in Computer Science, pages 1–6, Berlin, Heidelberg, April 2004. Springer. [ bib \| DOI \| Abstract ]
[137]	Peter Selinger. Towards a Quantum Programming Language. Mathematical Structures in Computer Science, 14(4):527–586, August 2004. [ bib \| DOI \| .pdf \| Abstract ]
[138]	Peter Selinger. Dagger Compact Closed Categories and Completely Positive Maps (Extended Abstract). Electronic Notes in Theoretical Computer Science, 170:139–163, March 2007. Proceedings of the 3rd International Workshop on Quantum Programming Languages (QPL 2005). [ bib \| DOI \| .pdf \| Abstract ]
[139]	Peter Selinger and Benoît Valiron. A Lambda Calculus for Quantum Computation with Classical Control. Mathematical Structures in Computer Science, 16(3):527–552, June 2006. [ bib \| DOI \| .pdf \| Abstract ]
[140]	Peter Selinger and Benoît Valiron. Quantum Lambda Calculus. In Gay and Mackie [55], pages 135–172. [ bib \| DOI \| .pdf \| Abstract ]
[141]	Kartik Singhal. Quantum Hoare Type Theory. Master's thesis, University of Chicago, Chicago, IL, December 2020. [ bib \| arXiv \| https \| Abstract ]
[142]	Kartik Singhal, Kesha Hietala, Sarah Marshall, and Robert Rand. Q# as a Quantum Algorithmic Language. In Stefano Gogioso and Matty Hoban, editors, Proceedings 19th International Conference on Quantum Physics and Logic, Wolfson College, Oxford, UK, 27 June–1 July 2022, volume 394 of Electronic Proceedings in Theoretical Computer Science, pages 170–191, Waterloo, NSW, Australia, November 2023. Open Publishing Association. [ bib \| DOI \| https \| Abstract ]
[143]	Kartik Singhal, Sarah Marshall, Kesha Hietala, and Robert Rand. Toward a Type-Theoretic Interpretation of Q# and Statically Enforcing the No-Cloning Theorem. In Second International Workshop on Programming Languages for Quantum Computing (PLanQC '21), June 2021. [ bib \| https \| Abstract ]
[144]	Kartik Singhal, Robert Rand, and Michael Hicks. Verified translation between low-level quantum languages. In First International Workshop on Programming Languages for Quantum Computing (PLanQC '20), January 2020. [ bib \| https \| Abstract ]
[145]	Kartik Singhal and John Reppy. Quantum Hoare Type Theory: Extended Abstract. In Benoît Valiron, Shane Mansfield, Pablo Arrighi, and Prakash Panangaden, editors, Proceedings of the 17th International Conference on Quantum Physics and Logic (QPL), Paris, France, June 2–6, 2020, volume 340 of Electronic Proceedings in Theoretical Computer Science, pages 291–302, Waterloo, NSW, Australia, September 2021. Open Publishing Association. [ bib \| DOI \| https \| Abstract ]
[146]	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, November 2020. [ bib \| DOI \| arXiv \| https \| Abstract ]
[147]	Robert S. Smith, Michael J. Curtis, and William J. Zeng. A Practical Quantum Instruction Set Architecture, August 2016. [ bib \| arXiv \| https \| Abstract ]
[148]	Robert S. Smith, Eric C. Peterson, Mark G. Skilbeck, and Erik J. Davis. An Open-Source, Industrial-Strength Optimizing Compiler for Quantum Programs. Quantum Science and Technology, 5(4):044001, July 2020. [ bib \| DOI \| https \| Abstract ]
[149]	Sam Staton. Algebraic Effects, Linearity, and Quantum Programming Languages. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '15, pages 395–406, New York, NY, USA, January 2015. Association for Computing Machinery. [ bib \| DOI \| .pdf \| Abstract ]
[150]	Damian S. Steiger, Thomas Häner, and Matthias Troyer. ProjectQ: An Open Source Software Framework for Quantum Computing. Quantum, 2:49, January 2018. [ bib \| DOI \| Abstract ]
[151]	Krysta M. Svore, Alfred V. Aho, Andrew W. Cross, Isaac L. Chuang, and Igor L. Markov. A Layered Software Architecture for Quantum Computing Design Tools. Computer, 39(1):74–83, January 2006. [ bib \| DOI \| .pdf \| Abstract ]
[152]	Krysta M. Svore, Andrew W. Cross, Alfred V. Aho, Isaac L. Chuang, and Igor L. Markov. Toward a Software Architecture for Quantum Computing Design Tools. In Proceedings of the 2nd International Workshop on Quantum Programming Languages (QPL), Turku, Finland, July 12–13, 2004, pages 145–162, July 2004. [ bib \| .pdf \| Abstract ]
[153]	Krysta M. Svore, Alan Geller, Matthias Troyer, John Azariah, Christopher E. Granade, Bettina Heim, Vadym Kliuchnikov, Mariia Mykhailova, Andres Paz, and Martin Roetteler. Q#: Enabling Scalable Quantum Computing and Development with a High-Level DSL. In Proceedings of the Real World Domain Specific Languages Workshop 2018, RWDSL '18, page 7, New York, NY, USA, February 2018. Association for Computing Machinery. [ bib \| DOI \| arXiv \| Abstract ]
[154]	Runzhou Tao, Yunong Shi, Jianan Yao, John Hui, Frederic T. Chong, and Ronghui Gu. Gleipnir: Toward Practical Error Analysis for Quantum Programs. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2021, pages 48–64, New York, NY, USA, June 2021. Association for Computing Machinery. [ bib \| DOI \| Abstract ]
[155]	Runzhou Tao, Yunong Shi, Jianan Yao, Xupeng Li, Ali Javadi-Abhari, Andrew W. Cross, Frederic T. Chong, and Ronghui Gu. Giallar: Push-Button Verification for the Qiskit Quantum Compiler. In Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI '22, pages 641–656, New York, NY, USA, June 2022. Association for Computing Machinery. [ bib \| DOI \| arXiv \| Abstract ]
[156]	Dominique Unruh. Quantum Hoare Logic with Ghost Variables. In Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '19, page 47, Los Alamitos, CA, USA, June 2019. IEEE Computer Society. [ bib \| DOI \| arXiv \| Abstract ]
[157]	Dominique Unruh. Quantum Relational Hoare Logic. Proceedings of the ACM on Programming Languages, 3(POPL):33, January 2019. [ bib \| DOI \| arXiv \| Abstract ]
[158]	Dominique Unruh. Quantum and classical registers, November 2021. [ bib \| arXiv \| Abstract ]
[159]	Dominique Unruh. Quantum and Classical Registers. Archive of Formal Proofs, 2021, October 2021. [ bib \| .html \| Abstract ]
[160]	Benoît Valiron, Neil J. Ross, Peter Selinger, D. Scott Alexander, and Jonathan M. Smith. Programming the Quantum Future. Communications of the ACM, 58(8):52–61, July 2015. [ bib \| DOI \| Abstract ]
[161]	John van de Wetering. ZX-calculus for the working quantum computer scientist, December 2020. [ bib \| arXiv \| Abstract ]
[162]	Juliana Kaizer Vizzotto, Thorsten Altenkirch, and Amr Sabry. Structuring quantum effects: superoperators as arrows. Mathematical Structures in Computer Science, 16(3):453–468, July 2006. [ bib \| DOI \| arXiv \| Abstract ]
[163]	Juliana Kaizer Vizzotto, André Rauber Du Bois, and Amr Sabry. The Arrow Calculus as a Quantum Programming Language. In Hiroakira Ono, Makoto Kanazawa, and Ruy de Queiroz, editors, Logic, Language, Information and Computation, pages 379–393, Berlin, Heidelberg, June 2009. Springer. [ bib \| DOI \| Abstract ]
[164]	Juliana Kaizer Vizzotto, Giovani Rubert Librelotto, and Amr Sabry. Reasoning about General Quantum Programs over Mixed States. In Marcel Vinícius Medeiros Oliveira and Jim Woodcock, editors, Formal Methods: Foundations and Applications: 12th Brazilian Symposium on Formal Methods, SBMF 2009 Gramado, Brazil, August 19-21, 2009 Revised Selected Papers, pages 321–335, Berlin, Heidelberg, November 2009. Springer. [ bib \| DOI \| Abstract ]
[165]	Finn Voichick, Liyi Li, Robert Rand, and Michael Hicks. Qunity: A Unified Language for Quantum and Classical Computing. Proceedings of the ACM on Programming Languages, 7(POPL):32, January 2023. [ bib \| DOI \| arXiv \| https \| Abstract ]
[166]	Dave Wecker and Krysta M. Svore. LIQUi\|⟩: A Software Design Architecture and Domain-Specific Language for Quantum Computing, February 2014. [ bib \| arXiv \| Abstract ]
[167]	Amanda Xu, Abtin Molavi, Lauren Pick, Swamit Tannu, and Aws Albarghouthi. Synthesizing Quantum-Circuit Optimizers. Proceedings of the ACM on Programming Languages, 7(PLDI):140, June 2023. [ bib \| DOI \| Abstract ]
[168]	Mingkuan Xu, Zikun Li, Oded Padon, Sina Lin, Jessica Pointing, Auguste Hirth, Henry Ma, Jens Palsberg, Alex Aiken, Umut A. Acar, and Zhihao Jia. Quartz: Superoptimization of Quantum Circuits. In Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI '22, pages 625–640, New York, NY, USA, June 2022. Association for Computing Machinery. [ bib \| DOI \| arXiv \| https \| Abstract ]
[169]	Peng Yan, Hanru Jiang, and Nengkun Yu. On Incorrectness Logic for Quantum Programs. Proceedings of the ACM on Programming Languages, 6(OOPSLA1):72, April 2022. [ bib \| DOI \| https \| Abstract ]
[170]	Mingsheng Ying. Hoare Logic for Quantum Programs, June 2009. [ bib \| arXiv \| Abstract ]
[171]	Mingsheng Ying. Floyd–Hoare Logic for Quantum Programs. ACM Transactions on Programming Languages and Systems, 33(6):19, January 2012. [ bib \| DOI \| Abstract ]
[172]	Mingsheng Ying. Quantum Recursion and Second Quantisation, May 2014. Talk at Tsinghua Software Day 2014. [ bib \| arXiv \| Abstract ]
[173]	Mingsheng Ying. Foundations of Quantum Programming. Morgan Kaufmann, Amsterdam, March 2016. [ bib \| DOI \| Abstract ]
[174]	Mingsheng Ying. Birkhoff-von Neumann Quantum Logic as an Assertion Language for Quantum Programs, May 2022. [ bib \| arXiv \| Abstract ]
[175]	Mingsheng Ying, Runyao Duan, Yuan Feng, and Zhengfeng Ji. Predicate Transformer Semantics of Quantum Programs. In Gay and Mackie [55], pages 311–360. [ bib \| DOI \| .pdf \| Abstract ]
[176]	Mingsheng Ying and Yuan Feng. Model Checking Quantum Systems: Principles and Algorithms. Cambridge University Press, Cambridge, January 2021. [ bib \| DOI \| Abstract ]
[177]	Mingsheng Ying, Shenggang Ying, and Xiaodi Wu. Invariants of Quantum Programs: Characterisations and Generation. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL '17, pages 818–832, New York, NY, USA, January 2017. Association for Computing Machinery. [ bib \| DOI \| .pdf \| Abstract ]
[178]	Mingsheng Ying, Nengkun Yu, and Yuan Feng. Alternation in Quantum Programming: From Superposition of Data to Superposition of Programs, February 2014. [ bib \| arXiv \| Abstract ]
[179]	Mingsheng Ying, Nengkun Yu, Yuan Feng, and Runyao Duan. Verification of Quantum Programs. Science of Computer Programming, 78(9):1679–1700, September 2013. [ bib \| DOI \| Abstract ]
[180]	Mingsheng Ying, Li Zhou, and Yangjia Li. Reasoning about Parallel Quantum Programs, October 2018. [ bib \| arXiv \| Abstract ]
[181]	Mingsheng Ying, Li Zhou, Yangjia Li, and Yuan Feng. A proof system for disjoint parallel quantum programs. Theoretical Computer Science, 897:164–184, November 2021. [ bib \| DOI \| Abstract ]
[182]	Nengkun Yu and Jens Palsberg. Quantum Abstract Interpretation. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI '21, pages 542–558, New York, NY, USA, June 2021. Association for Computing Machinery. [ bib \| DOI \| .pdf \| Abstract ]
[183]	Charles Yuan and Michael Carbin. Tower: Data Structures in Quantum Superposition. Proceedings of the ACM on Programming Languages, 6(OOPSLA2):134, October 2022. [ bib \| DOI \| arXiv \| https \| Abstract ]
[184]	Charles Yuan, Christopher McNally, and Michael Carbin. Twist: Sound Reasoning for Purity and Entanglement in Quantum Programs. Proceedings of the ACM on Programming Languages, 6(POPL):30, January 2022. [ bib \| DOI \| arXiv \| https \| Abstract ]
[185]	Jianjun Zhao. Quantum Software Engineering: Landscapes and Horizons, July 2020. [ bib \| arXiv \| Abstract ]
[186]	Li Zhou, Gilles Barthe, Justin Hsu, Mingsheng Ying, and Nengkun Yu. A Quantum Interpretation of Bunched Logic & Quantum Separation Logic. In Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '21, pages 1–14, Los Alamitos, CA, USA, July 2021. IEEE Computer Society. [ bib \| DOI \| arXiv \| Abstract ]
[187]	Li Zhou, Gilles Barthe, Pierre-Yves Strub, Junyi Liu, and Mingsheng Ying. CoqQ: Foundational Verification of Quantum Programs. Proceedings of the ACM on Programming Languages, 7(POPL):29, January 2023. [ bib \| DOI \| arXiv \| https \| Abstract ]
[188]	Li Zhou, Nengkun Yu, and Mingsheng Ying. An Applied Quantum Hoare Logic. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '19, pages 1149–1162, New York, NY, USA, June 2019. Association for Computing Machinery. [ bib \| DOI \| .pdf \| Abstract ]
[189]	Margherita Zorzi. Quantum Calculi—From Theory to Language Design. Applied Sciences, 9(24):5472, December 2019. [ bib \| DOI \| Abstract ]

This file was generated by bibtex2html 1.99.

Go home.