Document Open Access Logo

Denotational Semantics for Stabiliser Quantum Programs

Authors Robert I. Booth , Cole Comfort

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2026.8.pdf
  • Filesize: 1.15 MB
  • 24 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Denotational semantics
  • Theory of computation → Quantum computation theory
  • Theory of computation → Program reasoning
Keywords
  • quantum programming languages
  • quantum error correction
  • denotational semantics
  • categorical semantics
  • stabiliser theory
  • symplectic linear algebra

Metrics

Abstract

The stabiliser fragment of quantum theory is a foundational building block for quantum error correction, and hence for the fault-tolerant compilation of quantum programs. In this article, we develop a sound, universal, and complete denotational semantics for stabiliser operations, including measurement, classically controlled Pauli operators, and affine classical computation, thereby supporting an explicit treatment of quantum error-correcting codes. We interpret stabiliser operations as affine relations over finite fields, yielding a semantics that reflects the algebraic structure underlying stabiliser quantum error correction. Because stabiliser quantum mechanics has a well-behaved algebraic structure, our relational semantics is conceptually transparent and computationally tractable when compared to standard denotational models for general quantum programs. We demonstrate the resulting semantics by describing a small, low-level assembly language for stabiliser programs with fully abstract denotational semantics.

Cite As Get BibTex

Robert I. Booth and Cole Comfort. Denotational Semantics for Stabiliser Quantum Programs. In 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 8:1-8:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.FSCD.2026.8

Author Details

Robert I. Booth
  • University of Oxford, United Kingdom
Cole Comfort
  • Université Paris-Saclay, CNRS, ENS Paris-Saclay, Inria, CentraleSupélec, Laboratoire Méthodes Formelles, France

Funding

  • Booth, Robert I.: Engineering and Physical Sciences Research Council grant reference EP/Z002230/1: (De)constructing quantum software (DeQS).
  • Comfort, Cole: This work has been partially funded by the European Union through the MSCA SE project QCOMICAL and within the framework of "Plan France 2030", under the research projects EPIQ ANR-22-PETQ-0007 and HQI-R&D ANR-22-PNCQ-0002.

Acknowledgements

We thank our reviewers for helping to improve the exposition and correct typos. We also thank Louis Lemonnier and Vladimir Zamdzhiev for useful discussions.

References

  1. Scott Aaronson and Daniel Gottesman. Improved simulation of stabilizer circuits. Physical Review A, 70(5), November 2004. URL: https://doi.org/10.1103/physreva.70.052328.
  2. Rajeev Acharya, Dmitry A. Abanin, Laleh Aghababaie-Beni, Igor Aleiner, Trond I. Andersen, Markus Ansmann, Frank Arute, Kunal Arya, Abraham Asfaw, Nikita Astrakhantsev, Juan Atalaya, Ryan Babbush, Dave Bacon, Brian Ballard, Joseph C. Bardin, Johannes Bausch, Andreas Bengtsson, Alexander Bilmes, Sam Blackwell, Sergio Boixo, Gina Bortoli, Alexandre Bourassa, Jenna Bovaird, Leon Brill, Michael Broughton, David A. Browne, Brett Buchea, Bob B. Buckley, David A. Buell, Tim Burger, Brian Burkett, Nicholas Bushnell, Anthony Cabrera, Juan Campero, Hung-Shen Chang, Yu Chen, Zijun Chen, Ben Chiaro, Desmond Chik, Charina Chou, Jahan Claes, Agnetta Y. Cleland, Josh Cogan, Roberto Collins, Paul Conner, William Courtney, Alexander L. Crook, Ben Curtin, Sayan Das, Alex Davies, Laura De Lorenzo, Dripto M. Debroy, Sean Demura, Michel Devoret, Agustin Di Paolo, Paul Donohoe, Ilya Drozdov, Andrew Dunsworth, Clint Earle, Thomas Edlich, Alec Eickbusch, Aviv Moshe Elbag, Mahmoud Elzouka, Catherine Erickson, Lara Faoro, Edward Farhi, Vinicius S. Ferreira, Leslie Flores Burgos, Ebrahim Forati, Austin G. Fowler, Brooks Foxen, Suhas Ganjam, Gonzalo Garcia, Robert Gasca, Élie Genois, William Giang, Craig Gidney, Dar Gilboa, Raja Gosula, Alejandro Grajales Dau, Dietrich Graumann, Alex Greene, Jonathan A. Gross, Steve Habegger, John Hall, Michael C. Hamilton, Monica Hansen, Matthew P. Harrigan, Sean D. Harrington, Francisco J. H. Heras, Stephen Heslin, Paula Heu, Oscar Higgott, Gordon Hill, Jeremy Hilton, George Holland, Sabrina Hong, Hsin-Yuan Huang, Ashley Huff, William J. Huggins, Lev B. Ioffe, Sergei V. Isakov, Justin Iveland, Evan Jeffrey, Zhang Jiang, Cody Jones, Stephen Jordan, Chaitali Joshi, Pavol Juhas, Dvir Kafri, Hui Kang, Amir H. Karamlou, Kostyantyn Kechedzhi, Julian Kelly, Trupti Khaire, Tanuj Khattar, Mostafa Khezri, Seon Kim, Paul V. Klimov, Andrey R. Klots, Bryce Kobrin, Pushmeet Kohli, Alexander N. Korotkov, Fedor Kostritsa, Robin Kothari, Borislav Kozlovskii, John Mark Kreikebaum, Vladislav D. Kurilovich, Nathan Lacroix, David Landhuis, Tiano Lange-Dei, Brandon W. Langley, Pavel Laptev, Kim-Ming Lau, Loïck Le Guevel, Justin Ledford, Joonho Lee, Kenny Lee, Yuri D. Lensky, Shannon Leon, Brian J. Lester, Wing Yan Li, Yin Li, Alexander T. Lill, Wayne Liu, William P. Livingston, Aditya Locharla, Erik Lucero, Daniel Lundahl, Aaron Lunt, Sid Madhuk, Fionn D. Malone, Ashley Maloney, Salvatore Mandrà, James Manyika, Leigh S. Martin, Orion Martin, Steven Martin, Cameron Maxfield, Jarrod R. McClean, Matt McEwen, Seneca Meeks, Anthony Megrant, Xiao Mi, Kevin C. Miao, Amanda Mieszala, Reza Molavi, Sebastian Molina, Shirin Montazeri, Alexis Morvan, Ramis Movassagh, Wojciech Mruczkiewicz, Ofer Naaman, Matthew Neeley, Charles Neill, Ani Nersisyan, Hartmut Neven, Michael Newman, Jiun How Ng, Anthony Nguyen, Murray Nguyen, Chia-Hung Ni, Murphy Yuezhen Niu, Thomas E. O’Brien, William D. Oliver, Alex Opremcak, Kristoffer Ottosson, Andre Petukhov, Alex Pizzuto, John Platt, Rebecca Potter, Orion Pritchard, Leonid P. Pryadko, Chris Quintana, Ganesh Ramachandran, Matthew J. Reagor, John Redding, David M. Rhodes, Gabrielle Roberts, Eliott Rosenberg, Emma Rosenfeld, Pedram Roushan, Nicholas C. Rubin, Negar Saei, Daniel Sank, Kannan Sankaragomathi, Kevin J. Satzinger, Henry F. Schurkus, Christopher Schuster, Andrew W. Senior, Michael J. Shearn, Aaron Shorter, Noah Shutty, Vladimir Shvarts, Shraddha Singh, Volodymyr Sivak, Jindra Skruzny, Spencer Small, Vadim Smelyanskiy, W. Clarke Smith, Rolando D. Somma, Sofia Springer, George Sterling, Doug Strain, Jordan Suchard, Aaron Szasz, Alex Sztein, Douglas Thor, Alfredo Torres, M. Mert Torunbalci, Abeer Vaishnav, Justin Vargas, Sergey Vdovichev, Guifre Vidal, Benjamin Villalonga, Catherine Vollgraff Heidweiller, Steven Waltman, Shannon X. Wang, Brayden Ware, Kate Weber, Travis Weidel, Theodore White, Kristi Wong, Bryan W. K. Woo, Cheng Xing, Z. Jamie Yao, Ping Yeh, Bicheng Ying, Juhwan Yoo, Noureldin Yosri, Grayson Young, Adam Zalcman, Yaxing Zhang, Ningfeng Zhu, Nicholas Zobrist, and Google Quantum AI and Collaborators. Quantum error correction below the surface code threshold. Nature, 638(8052):920-926, 2025. Publisher: Nature Publishing Group. URL: https://doi.org/10.1038/s41586-024-08449-y.
  3. Rajeev Acharya, Igor Aleiner, Richard Allen, Trond I. Andersen, Markus Ansmann, Frank Arute, Kunal Arya, Abraham Asfaw, Juan Atalaya, Ryan Babbush, Dave Bacon, Joseph C. Bardin, Joao Basso, Andreas Bengtsson, Sergio Boixo, Gina Bortoli, Alexandre Bourassa, Jenna Bovaird, Leon Brill, Michael Broughton, Bob B. Buckley, David A. Buell, Tim Burger, Brian Burkett, Nicholas Bushnell, Yu Chen, Zijun Chen, Ben Chiaro, Josh Cogan, Roberto Collins, Paul Conner, William Courtney, Alexander L. Crook, Ben Curtin, Dripto M. Debroy, Alexander Del Toro Barba, Sean Demura, Andrew Dunsworth, Daniel Eppens, Catherine Erickson, Lara Faoro, Edward Farhi, Reza Fatemi, Leslie Flores Burgos, Ebrahim Forati, Austin G. Fowler, Brooks Foxen, William Giang, Craig Gidney, Dar Gilboa, Marissa Giustina, Alejandro Grajales Dau, Jonathan A. Gross, Steve Habegger, Michael C. Hamilton, Matthew P. Harrigan, Sean D. Harrington, Oscar Higgott, Jeremy Hilton, Markus Hoffmann, Sabrina Hong, Trent Huang, Ashley Huff, William J. Huggins, Lev B. Ioffe, Sergei V. Isakov, Justin Iveland, Evan Jeffrey, Zhang Jiang, Cody Jones, Pavol Juhas, Dvir Kafri, Kostyantyn Kechedzhi, Julian Kelly, Tanuj Khattar, Mostafa Khezri, Mária Kieferová, Seon Kim, Alexei Kitaev, Paul V. Klimov, Andrey R. Klots, Alexander N. Korotkov, Fedor Kostritsa, John Mark Kreikebaum, David Landhuis, Pavel Laptev, Kim-Ming Lau, Lily Laws, Joonho Lee, Kenny Lee, Brian J. Lester, Alexander Lill, Wayne Liu, Aditya Locharla, Erik Lucero, Fionn D. Malone, Jeffrey Marshall, Orion Martin, Jarrod R. McClean, Trevor McCourt, Matt McEwen, Anthony Megrant, Bernardo Meurer Costa, Xiao Mi, Kevin C. Miao, Masoud Mohseni, Shirin Montazeri, Alexis Morvan, Emily Mount, Wojciech Mruczkiewicz, Ofer Naaman, Matthew Neeley, Charles Neill, Ani Nersisyan, Hartmut Neven, Michael Newman, Jiun How Ng, Anthony Nguyen, Murray Nguyen, Murphy Yuezhen Niu, Thomas E. O’Brien, Alex Opremcak, John Platt, Andre Petukhov, Rebecca Potter, Leonid P. Pryadko, Chris Quintana, Pedram Roushan, Nicholas C. Rubin, Negar Saei, Daniel Sank, Kannan Sankaragomathi, Kevin J. Satzinger, Henry F. Schurkus, Christopher Schuster, Michael J. Shearn, Aaron Shorter, Vladimir Shvarts, Jindra Skruzny, Vadim Smelyanskiy, W. Clarke Smith, George Sterling, Doug Strain, Marco Szalay, Alfredo Torres, Guifre Vidal, Benjamin Villalonga, Catherine Vollgraff Heidweiller, Theodore White, Cheng Xing, Z. Jamie Yao, Ping Yeh, Juhwan Yoo, Grayson Young, Adam Zalcman, Yaxing Zhang, Ningfeng Zhu, and Google Quantum AI. Suppressing quantum errors by scaling a surface code logical qubit. Nature, 614(7949):676-681, 2023. Publisher: Nature Publishing Group. URL: https://doi.org/10.1038/s41586-022-05434-1.
  4. M. Laura Arias and Alejandra Maestripieri. On partial orders of operators. Annals of Functional Analysis, 14(1), December 2022. URL: https://doi.org/10.1007/s43034-022-00244-y.
  5. A. Ashikhmin and E. Knill. Nonbinary quantum stabilizer codes. IEEE Transactions on Information Theory, 47(7):3065-3072, 2001. URL: https://doi.org/10.1109/18.959288.
  6. P. N. Benton. A mixed linear and non-linear logic: Proofs, terms and models: Extended abstract, pages 121-135. Springer Berlin Heidelberg, 1995. URL: https://doi.org/10.1007/bfb0022251.
  7. Michael E. Beverland, Prakash Murali, Matthias Troyer, Krysta M. Svore, Torsten Hoefler, Vadym Kliuchnikov, Guang Hao Low, Mathias Soeken, Aarthi Sundaram, and Alexander Vaschillo. Assessing requirements to scale to practical quantum advantage, 2022. URL: https://doi.org/10.48550/arXiv.2211.07629.
  8. Hector Bombin, Daniel Litinski, Naomi Nickerson, Fernando Pastawski, and Sam Roberts. Unifying flavors of fault tolerance with the ZX calculus. Quantum, 8:1379, June 2024. URL: https://doi.org/10.22331/q-2024-06-18-1379.
  9. Robert I. Booth, Titouan Carette, and Cole Comfort. Graphical symplectic algebra. In Frank Pfenning, editor, 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026), Leibniz International Proceedings in Informatics (LIPIcs). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2026. To appear. URL: https://doi.org/10.4230/LIPIcs.FSCD.2026.4.
  10. S. B. Bravyi and A. Yu. Kitaev. Quantum codes on a lattice with boundary, 1998. URL: https://arxiv.org/abs/quant-ph/9811052.
  11. Sergey Bravyi, Andrew W. Cross, Jay M. Gambetta, Dmitri Maslov, Patrick Rall, and Theodore J. Yoder. High-threshold and low-overhead fault-tolerant quantum memory. Nature, 627(8005):778-782, 2024. Publisher: Nature Publishing Group. URL: https://doi.org/10.1038/s41586-024-07107-7.
  12. Paul Busch, Pekka Lahti, Juha-Pekka Pellonpää, and Kari Ylinen. Quantum Measurement. Springer International Publishing, 2016. URL: https://doi.org/10.1007/978-3-319-43389-9.
  13. A. R. Calderbank and Peter W. Shor. Good quantum error-correcting codes exist. Physical Review A, 54(2):1098-1105, August 1996. URL: https://doi.org/10.1103/physreva.54.1098.
  14. Earl T. Campbell, Barbara M. Terhal, and Christophe Vuillot. Roads towards fault-tolerant universal quantum computation. Nature, 549(7671):172-179, 2017. Publisher: Nature Publishing Group. URL: https://doi.org/10.1038/nature23460.
  15. Nicholas Chancellor, Aleks Kissinger, Stefan Zohren, Joschka Roffe, and Dominic Horsman. Graphical structures for design and verification of quantum error correction. Quantum Science and Technology, 8(4):045028, September 2023. URL: https://doi.org/10.1088/2058-9565/acf157.
  16. Kean Chen, Yuhao Liu, Wang Fang, Jennifer Paykin, Xin-Chuan Wu, Albert Schmitz, Steve Zdancewic, and Gushu Li. Verifying Fault-Tolerance of Quantum Error Correction Codes, pages 3-27. Springer Nature Switzerland, 2025. URL: https://doi.org/10.1007/978-3-031-98685-7_1.
  17. Bob Coecke, Chris Heunen, and Aleks Kissinger. Categories of quantum and classical channels. Quantum Information Processing, 15(12):5179-5209, October 2014. URL: https://doi.org/10.1007/s11128-014-0837-4.
  18. Cole Comfort. Stabiliser programming language (SPL). https://github.com/ColeComfort/SPL, 2025. GitHub repository.
  19. Cole Comfort and Aleks Kissinger. A graphical calculus for Lagrangian relations. In Electronic Proceedings in Theoretical Computer Science, volume 372, pages 338-351. EPTCS, 2022. URL: https://doi.org/10.4204/EPTCS.372.24.
  20. Eric Dennis, Alexei Kitaev, Andrew Landahl, and John Preskill. Topological quantum memory. Journal of Mathematical Physics, 43(9):4452-4505, September 2002. URL: https://doi.org/10.1063/1.1499754.
  21. Ross Duncan and Maxime Lucas. Verifying the Steane code with Quantomatic. Electronic Proceedings in Theoretical Computer Science, 171:33-49, December 2014. URL: https://doi.org/10.4204/eptcs.171.4.
  22. Wang Fang and Mingsheng Ying. Symbolic execution for quantum error correction programs. Proceedings of the ACM on Programming Languages, 8:189:1040-189:1065, 2024. URL: https://doi.org/10.1145/3656419.
  23. Daniel Gottesman. Stabilizer Codes and Quantum Error Correction. PhD thesis, California Institute of Technology, 1997. URL: https://arxiv.org/abs/quant-ph/9705052.
  24. Daniel Gottesman. An introduction to quantum error correction and fault-tolerant quantum computation, 2009. URL: https://arxiv.org/abs/0904.2557.
  25. David Gross. Hudson’s theorem for finite-dimensional quantum systems. Journal of Mathematical Physics, 47(12), December 2006. URL: https://doi.org/10.1063/1.2393152.
  26. Victor Guillemin and Shlomo Sternberg. Some problems in integral geometry and some related problems in micro-local analysis. American Journal of Mathematics, 101(4):915, August 1979. URL: https://doi.org/10.2307/2373923.
  27. Chris Heunen, Aleks Kissinger, and Peter Selinger. Completely positive projections and biproducts. Electronic Proceedings in Theoretical Computer Science, 171:71-83, 2014. URL: https://doi.org/10.4204/EPTCS.171.7.
  28. Qifan Huang, Li Zhou, Wang Fang, Mengyu Zhao, and Mingsheng Ying. Efficient formal verification of quantum error correcting programs. Proceedings of the ACM on Programming Languages, 9:1068-1093, 2025. URL: https://doi.org/10.1145/3729293.
  29. A.Yu. Kitaev. Fault-tolerant quantum computation by anyons. Annals of Physics, 303(1):2-30, January 2003. URL: https://doi.org/10.1016/s0003-4916(02)00018-0.
  30. Ian Mackie. Lilac: a functional programming language based on linear logic. Journal of Functional Programming, 4(4):395-433, 1994. URL: https://doi.org/10.1017/S0956796800001131.
  31. Yurii A. Neretin. Lectures on Gaussian Integral Operators and Classical Groups. EMS Press, February 2011. URL: https://doi.org/10.4171/080.
  32. Michael A. Nielsen and Isaac L. Chuang. Quantum Computation and Quantum Information: 10th Anniversary Edition. Cambridge University Press, June 2012. URL: https://doi.org/10.1017/cbo9780511976667.
  33. Alexandru Paler, Ilia Polian, Kae Nemoto, and Simon J Devitt. Fault-tolerant, high-level quantum circuits: form, compilation and description. Quantum Science and Technology, 2(2):025003, April 2017. URL: https://doi.org/10.1088/2058-9565/aa66eb.
  34. Jennifer Paykin and Sam Winnick. Qudit quantum programming with projective Cliffords. Proc. ACM Program. Lang., 10(POPL):89-116, January 2026. URL: https://doi.org/10.1145/3776646.
  35. Robert Rand, Aarthi Sundaram, Kartik Singhal, and Brad Lackey. Gottesman types for quantum programs. In Proceedings of the 17th International Conference on Quantum Physics and Logic (QPL 2020), volume 340, pages 279-290. Open Publishing Association, September 2021. URL: https://doi.org/10.4204/eptcs.340.14.
  36. Benjamin Rodatz, Boldizsár Poór, and Aleks Kissinger. Fault tolerance by construction. URL: https://arxiv.org/abs/2506.17181.
  37. Benjamin Rodatz, Boldizsár Poór, and Aleks Kissinger. Floquetifying stabiliser codes with distance-preserving rewrites. URL: https://arxiv.org/abs/2410.17240.
  38. Gerd Rudolph and Matthias Schmidt. Linear symplectic algebra. In Differential Geometry and Mathematical Physics: Part I. Manifolds, Lie Groups and Hamiltonian Systems, Theoretical and Mathematical Physics, pages 315-352. Springer Netherlands, 2013. URL: https://doi.org/10.1007/978-94-007-5345-7_7.
  39. C. Ryan-Anderson, J. G. Bohnet, K. Lee, D. Gresh, A. Hankin, J. P. Gaebler, D. Francois, A. Chernoguzov, D. Lucchetti, N. C. Brown, T. M. Gatterman, S. K. Halit, K. Gilmore, J. A. Gerber, B. Neyenhuis, D. Hayes, and R. P. Stutz. Realization of real-time fault-tolerant quantum error correction. Physical Review X, 11(4):041058, 2021. Publisher: American Physical Society. URL: https://doi.org/10.1103/PhysRevX.11.041058.
  40. Maximilian Rüsch, Benjamin Rodatz, and Aleks Kissinger. Completeness for fault equivalence of Clifford ZX diagrams. URL: https://arxiv.org/abs/2510.08477.
  41. Peter Selinger. Towards a quantum programming language. Mathematical. Structures in Comp. Sci., 14(4):527-586, August 2004. URL: https://doi.org/10.1017/S0960129504004256.
  42. Peter Selinger. Dagger compact closed categories and completely positive maps. Electronic Notes in Theoretical Computer Science, 170:139-163, March 2007. URL: https://doi.org/10.1016/j.entcs.2006.12.018.
  43. Peter Selinger. Idempotents in dagger categories. In Proceedings of the 4th International Workshop on Quantum Programming Languages (QPL 2006), volume 210, pages 107-122, 2008. URL: https://doi.org/10.1016/j.entcs.2008.04.021.
  44. A. M. Steane. Error correcting codes in quantum theory. Physical Review Letters, 77(5):793-797, July 1996. URL: https://doi.org/10.1103/physrevlett.77.793.
  45. Aarthi Sundaram, Robert Rand, Kartik Singhal, and Brad Lackey. Hoare meets Heisenberg: A lightweight logic for quantum programs, 2025. URL: https://arxiv.org/abs/2101.08939.
  46. Anbang Wu, Gushu Li, Hezi Zhang, Gian Giacomo Guerreschi, Yuan Xie, and Yufei Ding. QECV: Quantum error correction verification, 2021. URL: https://arxiv.org/abs/2111.13728.
  47. Mingsheng Ying. Foundations of Quantum Programming. Elsevier Inc., 2016. URL: https://doi.org/10.1016/C2014-0-02660-3.
  48. Uma Zalakain and Ornela Dardha. π with leftovers: A mechanisation in Agda. In Formal Techniques for Distributed Objects, Components, and Systems, pages 157-174. Springer International Publishing, 2021. URL: https://doi.org/10.1007/978-3-030-78089-0_9.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact