Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Log inSign up
Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Blog
Job Board
Q3AS

© 2026 Aqora Quantum S.A.S.

TermsPrivacyLegal Notice

arXiv:2311.14215 · ACM Transactions on Software Engineering and Methodology

Refinement Calculus of Quantum Programs with Projective Assertions

Yuan Feng, Li Zhou, Yingte Xu, Xiaoquan Xu

Published Oct 1, 2025• 3 citations
arXivHTMLPDF

Abstract

This article presents a refinement calculus designed specifically for quantum programs, offering a structured approach to their progressive and modular development while ensuring correctness throughout the refinement process. We begin by investigating the partial correctness of nondeterministic programs within a quantum while language featuring prescription statements. Orthogonal projectors, which are in one-to-one correspondence to subspaces of the state Hilbert space, are taken as assertions for quantum states. We provide the weakest liberal precondition and strongest postcondition semantics of quantum programs, and based on these dual semantics, introduce refinement rules that facilitate the incremental development of quantum programs. All these rules, as well as their soundness and completeness, are formalized and proven in the Coq proof assistant by utilizing CoqQ, a general-purpose framework for quantum computing and program verification. To demonstrate the utility of the refinement calculus, we examine examples including the implementation of a \( Z \) -rotation gate, the repetition error-correction code, and the quantum-to-quantum Bernoulli factory. Moreover, we present QRefine , a Python-based interactive prototype designed as a proof of concept to demonstrate the potential of our approach in the stepwise development of correct quantum programs.

DOI
10.1145/3770083

Related papers

Verification of Nondeterministic Quantum Programs

Yuan Feng, Yingte Xu

Nondeterministic choice is a useful program construct that provides a way to describe the behaviour of a program without specifying the details of possible implementations. It supports the stepwise refinement of programs, a method that has proven useful in software development. Nondeterminism has also been introduced in quantum programming, and termination of nondeterministic quantum programs has been extensively analysed. In this paper, we go beyond termination analysis to investigate the verification of nondeterministic quantum programs where properties are given by sets of hermitian operators on the associated Hilbert space. Hoare-type logic systems for partial and total correctness are proposed which turn out to be both sound and relatively complete with respect to their corresponding semantic correctness. To show the utility of these proof systems, we analyse some quantum algorithms such as quantum error correction scheme, Deutsch algorithm, and a nondeterministic quantum walk. Finally, a proof assistant prototype is implemented to aid in the automated reasoning of nondeterministic quantum programs.

arXiv:2302.07973•International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS)•Mar 20, 2023•11 citations

Refinement Orders for Quantum Programs

Yuan Feng, Li Zhou

Refinement is a fundamental technique in the verification and systematic development of computer programs. It supports a disciplined approach to software construction through stepwise refinement, whereby an abstract specification is gradually transformed into a concrete implementation that satisfies the desired requirements. Central to this methodology is the notion of a refinement order, which guarantees that each refinement step preserves program correctness. This paper presents the first comprehensive study of refinement orders for quantum programs, covering both deterministic and nondeterministic settings under total and partial correctness criteria. We investigate three natural classes of quantum predicates: projectors, representing qualitative properties; effects, capturing quantitative properties; and sets of effects, modeling demonic nondeterminism. For deterministic quantum programs, we show that refinement with respect to effect-based and set-of-effects based specifications coincides with the standard complete-positivity order on superoperators, whereas refinement induced by projector-based specifications can be characterized by the linear span of Kraus operators. For nondeterministic quantum programs with set-of-effects based specifications, we establish precise correspondences with classical domain-theoretic notions: the Smyth order characterizes refinement under total correctness, while the Hoare order characterizes refinement under partial correctness. Moreover, effect-based and projector-based specifications lead to strictly weaker refinement orders. From a theoretical perspective, our results provide a solid semantic foundation for the development of quantum refinement calculi. From a practical standpoint, they offer concrete guidance for quantum program designers in selecting appropriate predicate classes and correctness notions to support their intended refinement goals.

arXiv:2504.14158•ACM Transactions on Software Engineering and Methodology•Aug 25, 2026•0 citations

QbC: Quantum Correctness by Construction

Anurudh Peduri, Ina Schaefer, Michael Walter

Thanks to the rapid progress and growing complexity of quantum algorithms, correctness of quantum programs has become a major concern. Pioneering research over the past years has proposed various approaches to formally verify quantum programs using proof systems such as quantum Hoare logic. All these prior approaches are post-hoc: one first implements a program and only then verifies its correctness. Here we propose Quantum Correctness by Construction (QbC) : an approach to constructing quantum programs from their specification in a way that ensures correctness. We use pre- and postconditions to specify program properties, and propose sound and complete refinement rules for constructing programs in a quantum while language from their specification. We validate QbC by constructing quantum programs for idiomatic problems and patterns. We find that the approach naturally suggests how to derive program details, highlighting key design choices along the way. As such, we believe that QbC can play a role in supporting the design and taxonomization of quantum algorithms and software.

Proceedings of the ACM on Programming Languages•Apr 9, 2025•3 citations

QbC: Quantum Correctness by Construction

Anurudh Peduri, Ina Schaefer, Walter, Michael

Thanks to the rapid progress and growing complexity of quantum algorithms, correctness of quantum programs has become a major concern. Pioneering research over the past years has proposed various approaches to formally verify quantum programs using proof systems such as quantum Hoare logic. All these prior approaches are post-hoc: one first implements a program and only then verifies its correctness. Here we propose Quantum Correctness by Construction (QbC): an approach to constructing quantum programs from their specification in a way that ensures correctness. We use pre- and postconditions to specify program properties, and propose sound and complete refinement rules for constructing programs in a quantum while language from their specification. We validate QbC by constructing quantum programs for idiomatic problems and patterns. We find that the approach naturally suggests how to derive program details, highlighting key design choices along the way. As such, we believe that QbC can play a role in supporting the design and taxonomization of quantum algorithms and software.

arXiv:2307.15641•Jul 28, 2023•1 citation

CoqQ: Foundational Verification of Quantum Programs

Li Zhou, Gilles Barthe, Pierre-Yves Strub +2 more

CoqQ is a framework for reasoning about quantum programs in the Coq proof assistant. Its main components are: a deeply embedded quantum programming language, in which classic quantum algorithms are easily expressed, and an expressive program logic for proving properties of programs. CoqQ is foundational: the program logic is formally proved sound with respect to a denotational semantics based on state-of-art mathematical libraries (MathComp and MathComp Analysis). CoqQ is also practical: assertions can use Dirac expressions, which eases concise specifications, and proofs can exploit local and parallel reasoning, which minimizes verification effort. We illustrate the applicability of CoqQ with many examples from the literature.

arXiv:2207.11350•Proceedings of the ACM on Programming Languages•Jan 9, 2023•35 citations

Formal Verification of Continuous-Variable Quantum Programs

Stefanie Muroya, Thomas A. Henzinger

We provide a formal framework for Continuous-Variable Quantum Computing (CQC). While CQC is supported by photonic quantum hardware, we are not aware of a formal semantics for continuous-variable quantum programs nor of a unary Hoare logic for their verification. There are several technical obstacles to extending to CQC any of the formal frameworks available for Discrete-Variable Quantum Computing (DQC). Most importantly, continuous-variable quantum programs act on {\em infinite-dimensional} Hilbert spaces; their measurement outcomes are often {\em unbounded} and have expected values that are defined by an improper integral (or an infinite series), which may not converge. We overcome these challenges to give a formal semantics to a universal programming language for CQC and to provide the first Hoare logic for CQC. The assertions of our logic are built from polynomials over canonical observables. Besides proving relative completeness, we implement a symbolic weakest-precondition calculator for CQC based on our logic. Our tool has successfully verified CQC algorithms from textbooks and calculated their approximation errors for physically realizable implementations, proved the correctness (i.e., equivalence) of gate decompositions for CQC hardware, and computed the resource requirements (i.e., number of photon-number states) for achieving a desired accuracy in the classical simulation of continuous-variable quantum programs.

quant-pharXiv:2607.17714•Jul 21, 2026•0 citations
This article presents a refinement calculus designed specifically for quantum programs, offering a structured approach to their progressive and modular development while ensuring correctness throughout the refinement process. We begin by investigating the partial correctness of nondeterministic programs within a quantum while language featuring prescription statements. Orthogonal projectors, which are in one-to-one correspondence to subspaces of the state Hilbert space, are taken as assertions for quantum states. We provide the weakest liberal precondition and strongest postcondition semantics of quantum programs, and based on these dual semantics, introduce refinement rules that facilitate the incremental development of quantum programs. All these rules, as well as their soundness and completeness, are formalized and proven in the Coq proof assistant by utilizing CoqQ, a general-purpose framework for quantum computing and program verification. To demonstrate the utility of the refinement calculus, we examine examples including the implementation of a ( Z ) -rotation gate, the repetition error-correction code, and the quantum-to-quantum Bernoulli factory. Moreover, we present QRefine , a Python-based interactive prototype designed as a proof of concept to demonstrate the potential of our approach in the stepwise development of correct quantum programs.
Nondeterministic choice is a useful program construct that provides a way to describe the behaviour of a program without specifying the details of possible implementations. It supports the stepwise refinement of programs, a method that has proven useful in software development. Nondeterminism has also been introduced in quantum programming, and termination of nondeterministic quantum programs has been extensively analysed. In this paper, we go beyond termination analysis to investigate the verification of nondeterministic quantum programs where properties are given by sets of hermitian operators on the associated Hilbert space. Hoare-type logic systems for partial and total correctness are proposed which turn out to be both sound and relatively complete with respect to their corresponding semantic correctness. To show the utility of these proof systems, we analyse some quantum algorithms such as quantum error correction scheme, Deutsch algorithm, and a nondeterministic quantum walk. Finally, a proof assistant prototype is implemented to aid in the automated reasoning of nondeterministic quantum programs.
Refinement is a fundamental technique in the verification and systematic development of computer programs. It supports a disciplined approach to software construction through stepwise refinement, whereby an abstract specification is gradually transformed into a concrete implementation that satisfies the desired requirements. Central to this methodology is the notion of a refinement order, which guarantees that each refinement step preserves program correctness. This paper presents the first comprehensive study of refinement orders for quantum programs, covering both deterministic and nondeterministic settings under total and partial correctness criteria. We investigate three natural classes of quantum predicates: projectors, representing qualitative properties; effects, capturing quantitative properties; and sets of effects, modeling demonic nondeterminism. For deterministic quantum programs, we show that refinement with respect to effect-based and set-of-effects based specifications coincides with the standard complete-positivity order on superoperators, whereas refinement induced by projector-based specifications can be characterized by the linear span of Kraus operators. For nondeterministic quantum programs with set-of-effects based specifications, we establish precise correspondences with classical domain-theoretic notions: the Smyth order characterizes refinement under total correctness, while the Hoare order characterizes refinement under partial correctness. Moreover, effect-based and projector-based specifications lead to strictly weaker refinement orders. From a theoretical perspective, our results provide a solid semantic foundation for the development of quantum refinement calculi. From a practical standpoint, they offer concrete guidance for quantum program designers in selecting appropriate predicate classes and correctness notions to support their intended refinement goals.
Thanks to the rapid progress and growing complexity of quantum algorithms, correctness of quantum programs has become a major concern. Pioneering research over the past years has proposed various approaches to formally verify quantum programs using proof systems such as quantum Hoare logic. All these prior approaches are post-hoc: one first implements a program and only then verifies its correctness. Here we propose Quantum Correctness by Construction (QbC) : an approach to constructing quantum programs from their specification in a way that ensures correctness. We use pre- and postconditions to specify program properties, and propose sound and complete refinement rules for constructing programs in a quantum while language from their specification. We validate QbC by constructing quantum programs for idiomatic problems and patterns. We find that the approach naturally suggests how to derive program details, highlighting key design choices along the way. As such, we believe that QbC can play a role in supporting the design and taxonomization of quantum algorithms and software.
Thanks to the rapid progress and growing complexity of quantum algorithms, correctness of quantum programs has become a major concern. Pioneering research over the past years has proposed various approaches to formally verify quantum programs using proof systems such as quantum Hoare logic. All these prior approaches are post-hoc: one first implements a program and only then verifies its correctness. Here we propose Quantum Correctness by Construction (QbC): an approach to constructing quantum programs from their specification in a way that ensures correctness. We use pre- and postconditions to specify program properties, and propose sound and complete refinement rules for constructing programs in a quantum while language from their specification. We validate QbC by constructing quantum programs for idiomatic problems and patterns. We find that the approach naturally suggests how to derive program details, highlighting key design choices along the way. As such, we believe that QbC can play a role in supporting the design and taxonomization of quantum algorithms and software.
CoqQ is a framework for reasoning about quantum programs in the Coq proof assistant. Its main components are: a deeply embedded quantum programming language, in which classic quantum algorithms are easily expressed, and an expressive program logic for proving properties of programs. CoqQ is foundational: the program logic is formally proved sound with respect to a denotational semantics based on state-of-art mathematical libraries (MathComp and MathComp Analysis). CoqQ is also practical: assertions can use Dirac expressions, which eases concise specifications, and proofs can exploit local and parallel reasoning, which minimizes verification effort. We illustrate the applicability of CoqQ with many examples from the literature.
We provide a formal framework for Continuous-Variable Quantum Computing (CQC). While CQC is supported by photonic quantum hardware, we are not aware of a formal semantics for continuous-variable quantum programs nor of a unary Hoare logic for their verification. There are several technical obstacles to extending to CQC any of the formal frameworks available for Discrete-Variable Quantum Computing (DQC). Most importantly, continuous-variable quantum programs act on {\em infinite-dimensional} Hilbert spaces; their measurement outcomes are often {\em unbounded} and have expected values that are defined by an improper integral (or an infinite series), which may not converge. We overcome these challenges to give a formal semantics to a universal programming language for CQC and to provide the first Hoare logic for CQC. The assertions of our logic are built from polynomials over canonical observables. Besides proving relative completeness, we implement a symbolic weakest-precondition calculator for CQC based on our logic. Our tool has successfully verified CQC algorithms from textbooks and calculated their approximation errors for physically realizable implementations, proved the correctness (i.e., equivalence) of gate decompositions for CQC hardware, and computed the resource requirements (i.e., number of photon-number states) for achieving a desired accuracy in the classical simulation of continuous-variable quantum programs.