Denotational semantics for stabiliser quantum programs

• URL: http://arxiv.org/abs/2511.22734v1
• Date: Thu, 27 Nov 2025 19:51:43 GMT
• Title: Denotational semantics for stabiliser quantum programs
• Authors: Robert I. Booth, Cole Comfort,
• Abstract summary: We develop a sound, universal and complete denotational semantics for stabiliser operations.<n>We demonstrate the power of the resulting semantics by describing a small, proof-of-concept assembly language for stabiliser programs.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: The stabiliser fragment of quantum theory is a foundational building block for quantum error correction and the fault-tolerant compilation of quantum programs. In this article, we develop a sound, universal and complete denotational semantics for stabiliser operations which include measurement, classically-controlled Pauli operators, and affine classical operations, in which quantum error-correcting codes are first-class objects. The operations are interpreted as certain affine relations over finite fields. This offers a conceptually motivated and computationally-tractable alternative to the standard operator-algebraic semantics of quantum programs (whose time complexity grows exponentially as the state space increases in size). We demonstrate the power of the resulting semantics by describing a small, proof-of-concept assembly language for stabiliser programs with fully-abstract denotational semantics.

Related papers

• The Structure and Interpretation of Quantum Programs I: Foundations [0.0]
  Qubits are a great way to build a quantum computer, but a limited way to program one.<n>We replace the usual "states and gates" formalism with a "props and ops" (propositions and operators) model.<n>We show how measurement modifies state, proving an operator-algebraic version of the Knill-Laflamme conditions.
  arXiv  Detail & Related papers  (2025-09-03T18:00:23Z)
• Quantum circuits are just a phase [0.0]
  We introduce a novel quantum programming language for generating unitaries from "just a phase"<n>This minimal language lifts the focus from quantum gates to eigendecomposition, conjugation, and controlled unitaries.
  arXiv  Detail & Related papers  (2025-07-15T19:31:53Z)
• Operationally classical simulation of quantum states [41.94295877935867]
  A classical state-preparation device cannot generate superpositions and hence its emitted states must commute.<n>We show that no such simulation exists, thereby certifying quantum coherence.<n>Our approach is a possible avenue to understand how and to what extent quantum states defy generic models based on classical devices.
  arXiv  Detail & Related papers  (2025-02-03T15:25:03Z)
• BI-based Reasoning about Quantum Programs with Heap Manipulations [5.744265100221585]
  We provide well-founded semantics for a quantum programming language Qwhile-hp with heap manipulations. We develop a quantum BI-style logic that includes interpretations for separating implication. We then adopt this quantum BI-style logic as an assertion language to reason about heap-manipulated quantum programs.
  arXiv  Detail & Related papers  (2024-09-16T10:34:45Z)
• A bound on the quantum value of all compiled nonlocal games [49.32403970784162]
  A cryptographic compiler converts any nonlocal game into an interactive protocol with a single computationally bounded prover.<n>We establish a quantum soundness result for all compiled two-player nonlocal games.
  arXiv  Detail & Related papers  (2024-08-13T08:11:56Z)
• Relativistic Quantum Fields Are Universal Entanglement Embezzlers [41.94295877935867]
  Embezzlement of entanglement refers to the counterintuitive possibility of extracting entangled quantum states from a reference state of an auxiliary system.<n>We uncover a deep connection between the operational task of embezzling entanglement and the mathematical classification of von Neumann algebras.
  arXiv  Detail & Related papers  (2024-01-14T13:58:32Z)
• Refinement calculus of quantum programs with projective assertions [5.151896714190243]
  This paper introduces a refinement calculus tailored for quantum programs. We first study the partial correctness of nondeterministic programs within a quantum. We also present their semantics in transforming a postcondition to the weakest liberal postconditions.
  arXiv  Detail & Related papers  (2023-11-23T22:12:57Z)
• The Quantum Monadology [0.0]
  Modern theory of functional programming languages uses monads for encoding computational side-effects and side-contexts. We analyze the (co)monads on categories of parameterized module spectra induced by Grothendieck's "motivic yoga of operations" We indicate a domain-specific quantum programming language (QS) expressing these monadic quantum effects in transparent do-notation.
  arXiv  Detail & Related papers  (2023-10-24T11:19:24Z)
• Semidefinite programming relaxations for quantum correlations [42.72938925647165]
  We discuss how the core idea of semidefinite relaxations can be adapted for a variety of research topics in quantum correlations.<n>These topics include nonlocality, quantum communication, quantum networks, entanglement, and quantum cryptography.
  arXiv  Detail & Related papers  (2023-07-05T18:00:07Z)
• Interactive Protocols for Classically-Verifiable Quantum Advantage [46.093185827838035]
  "Interactions" between a prover and a verifier can bridge the gap between verifiability and implementation. We demonstrate the first implementation of an interactive quantum advantage protocol, using an ion trap quantum computer.
  arXiv  Detail & Related papers  (2021-12-09T19:00:00Z)
• Experimental violations of Leggett-Garg's inequalities on a quantum computer [77.34726150561087]
  We experimentally observe the violations of Leggett-Garg-Bell's inequalities on single and multi-qubit systems. Our analysis highlights the limits of nowadays quantum platforms, showing that the above-mentioned correlation functions deviate from theoretical prediction as the number of qubits and the depth of the circuit grow.
  arXiv  Detail & Related papers  (2021-09-06T14:35:15Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.