arXiv:2511.23472 · Proceedings of the ACM on Programming Languages

RapunSL: Untangling Quantum Computing with Separation, Linear Combination and Mixing

Yusuke Matsushita, Kengo Hirata, Ryo Wakizaka, Emanuele D'Osualdo

cs.PLcs.LOquant-phSubmitted Nov 28, 2025• Announced Dec 1, 2025• 2 citations

Abstract

Quantum Separation Logic (QSL) has been proposed as an effective tool to improve the scalability of deductive reasoning for quantum programs. In QSL, separation is interpreted as disentanglement, and the frame rule brings a notion of entanglement-local specification (one that only talks about the qubits entangled with those acted upon by the program). In this paper, we identify two notions of locality unique to the quantum domain, and we construct a novel quantum separation logic, RapunSL, which is able to soundly reduce reasoning about superposition states to reasoning about pure states (basis-locality), and reasoning about mixed states arising from measurement to reasoning about pure states (outcome-locality). To do so, we introduce two connectives, linear combination and mixing, which together with separation provide a dramatic improvement in the scalability of reasoning, as we demonstrate on a series of challenging case studies.

DOI: 10.1145/3776648
Comments: Full version of the conference paper at POPL 2026. The first two authors contributed equally to this work

Related papers

A Quantum interpretation of separating conjunction for local reasoning of Quantum programs based on separation logic

Xuan-Bach D. Le, Shang‐Wei Lin, Jun Sun +1 more

It is well-known that quantum programs are not only complicated to design but also challenging to verify because the quantum states can have exponential size and require sophisticated mathematics to encode and manipulate. To tackle the state-space explosion problem for quantum reasoning, we propose a Hoare-style inference framework that supports local reasoning for quantum programs. By providing a quantum interpretation of the separating conjunction, we are able to infuse separation logic into our framework and apply local reasoning using a quantum frame rule that is similar to the classical frame rule. For evaluation, we apply our framework to verify various quantum programs including Deutsch–Jozsa’s algorithm and Grover's algorithm.

Proceedings of the ACM on Programming LanguagesJan 12, 202216 citations

Twist: sound reasoning for purity and entanglement in Quantum programs

Charles Yuan, Christopher M. McNally, Michael Carbin

Quantum programming languages enable developers to implement algorithms for quantum computers that promise computational breakthroughs in classically intractable tasks. Programming quantum computers requires awareness of entanglement , the phenomenon in which measurement outcomes of qubits are correlated. Entanglement can determine the correctness of algorithms and suitability of programming patterns. In this work, we formalize purity as a central tool for automating reasoning about entanglement in quantum programs. A pure expression is one whose evaluation is unaffected by the measurement outcomes of qubits that it does not own, implying freedom from entanglement with any other expression in the computation. We present Twist, the first language that features a type system for sound reasoning about purity. The type system enables the developer to identify pure expressions using type annotations. Twist also features purity assertion operators that state the absence of entanglement in the output of quantum gates. To soundly check these assertions, Twist uses a combination of static analysis and runtime verification. We evaluate Twist’s type system and analyses on a benchmark suite of quantum programs in simulation, demonstrating that Twist can express quantum algorithms, catch programming errors in them, and support programs that existing languages disallow, while incurring runtime verification overhead of less than 3.5%.

arXiv:2205.02287Proceedings of the ACM on Programming LanguagesJan 12, 202231 citations

SAQR-QC: A Logic for Scalable but Approximate Quantitative Reasoning about Quantum Circuits

Nengkun Yu, Jens Palsberg, Thomas Reps

Reasoning about quantum programs remains a fundamental challenge, regardless of the programming model or computational paradigm. Existing verification techniques are insufficient—even for quantum circuits, a deliberately restricted model that lacks classical control, but still underpins many current quantum algorithms. Many existing formal methods require exponential time and space to represent and manipulate (representations of) assertions and judgments, making them impractical for quantum circuits with many qubits. This paper presents SAQR-QC, a logic for S calable but A pproximate Q uantitative R easoning about Q uantum C ircuits. SAQR-QC has three characteristics: (i) some deliberate loss of precision is built into it; (ii) it has a mechanism to help the accumulated loss of precision during a sequence of reasoning steps remain small; and (iii) every reasoning step is local—involving just a small number of qubits—making reasoning scalable. We demonstrate the effectiveness of SAQR-QC via two case studies: the verification of GHZ circuits involving non-Clifford gates, and the analysis of quantum phase estimation—a core subroutine in Shor’s factoring algorithm.

arXiv:2507.13635Proceedings of the ACM on Programming LanguagesJun 8, 20263 citations

Reasoning about Parallel Quantum Programs

Mingsheng Ying, Li Zhou, Yangjia Li

We initiate the study of parallel quantum programming by defining the operational and denotational semantics of parallel quantum programs. The technical contributions of this paper include: (1) find a series of useful proof rules for reasoning about correctness of parallel quantum programs; (2) prove a (relative) completeness of our proof rules for partial correctness of disjoint parallel quantum programs; and (3) prove a strong soundness theorem of the proof rules showing that partial correctness is well maintained at each step of transitions in the operational semantics of a general parallel quantum program (with shared variables). This is achieved by partially overcoming the following conceptual challenges that are never present in classical parallel programming: (i) the intertwining of nondeterminism caused by quantum measurements and introduced by parallelism; (ii) entanglement between component quantum programs; and (iii) combining quantum predicates in the overlap of state Hilbert spaces of component quantum programs with shared variables. Applications of the techniques developed in this paper are illustrated by a formal verification of Bravyi-Gosset-König's parallel quantum algorithm solving a linear algebra problem, which gives for the first time an unconditional proof of a computational quantum advantage.

arXiv:1810.11334Oct 26, 20188 citations

Local Reasoning about Probabilistic Behaviour for Classical-Quantum Programs

Huiling Wu, Yuxin Deng, Ming Xu

Verifying the functional correctness of programs with both classical and quantum constructs is a challenging task. The presence of probabilistic behaviour entailed by quantum measurements, together with the exponential size of quantum state spaces, complicates the verification task greatly. In this paper, we propose a quantum Hoare logic that supports separation-style local reasoning and introduces distribution formulas for specifying probabilistic properties, thereby enabling local reasoning about the probabilistic behaviour of classical-quantum programs. We show that the proof rules in the logic are sound with respect to a denotational semantics. To demonstrate the expressiveness of the logic, we formally verify several non-trivial examples, with a Bell-pair purification protocol serving as the main case study. Moreover, we embed our logic into the Rocq Prover (formerly Coq). The resulting logical framework, called CoqQLR, can facilitate semi-automated reasoning about classical--quantum programs.

arXiv:2308.04741Aug 9, 20230 citations

Quantum Entanglement-Based Logical Computation

Jincheng Zhang

Quantum entanglement, a bizarre phenomenon where two or more particles become linked regardless of the distance separating them, holds immense potential for revolutionizing computation. This paper explores the possibility of utilizing quantum entanglement to create a novel logical computation framework, leveraging the unique properties of entangled states to enhance computational efficiency. We propose a new conceptual model for logical operations based on entangled qubits, aiming to surpass the limitations of classical logic in handling complex computations. The core of this work focuses on the design of a quantum logic system that employs entanglement to facilitate a deeper level of logical reasoning than currently achievable with conventional methods. This investigation presents a preliminary framework, highlighting the potential for significant advancements in computational power through the integration of quantum entanglement.

Sep 3, 20260 citations