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:2501.15238 · ACM/IEEE Symposium on Logic in Computer Science (LICS)

Complete Quantum Relational Hoare Logics from Optimal Transport Duality

Gilles Barthe, Minbo Gao, Tianyi Wang, Li Zhou

Published Jun 23, 2025• 0 citations
arXivHTMLPDF

Abstract

We introduce a quantitative relational Hoare logic for quantum programs. Assertions of the logic range over a new infinitary extension of positive semidefinite operators. We prove that our logic is sound, and complete for bounded postconditions and almost surely terminating programs. Our completeness result is based on a quantum version of the duality theorem from optimal transport. We also define a complete embedding into our logic of a relational Hoare logic with projective assertions.

DOI
10.1109/lics65433.2025.00072

Related papers

Complete Relational Logic for Infinite-Dimensional Quantum Programs with Unbounded Assertions

Gilles Barthe, Minbo Gao, Jam Kabeer Ali Khan +7 more

We present sound and complete relational program logics for infinite-dimensional quantum and classical-quantum programs. The logics model assertions as self-adjoint unbounded linear relations, which simultaneously support quantitative and qualitative reasoning. Our main theoretical results include new convergence theorems and infinite-dimensional duality theorems for infinite-dimensional quantum states, which we use to establish completeness.

arXiv:2510.07051•Leibniz international proceedings in informatics•Oct 8, 2025•1 citation

Quantum Hoare Logic with Classical Variables

Yuan Feng, Mingsheng Ying

Hoare logic provides a syntax-oriented method to reason about program correctness and has been proven effective in the verification of classical and probabilistic programs. Existing proposals for quantum Hoare logic either lack completeness or support only quantum variables, thus limiting their capability in practical use. In this article, we propose a quantum Hoare logic for a simple while language that involves both classical and quantum variables. Its soundness and relative completeness are proven for both partial and total correctness of quantum programs written in the language. Remarkably, with novel definitions of classical-quantum states and corresponding assertions, the logic system is quite simple and similar to the traditional Hoare logic for classical programs. Furthermore, to simplify reasoning in real applications, auxiliary proof rules are provided that support standard logical operation in the classical part of assertions and super-operator application in the quantum part. Finally, a series of practical quantum algorithms, in particular the whole algorithm of Shor’s factorisation, are formally verified to show the effectiveness of the logic.

arXiv:2008.06812•ACM Transactions on Quantum Computing•Dec 21, 2021•44 citations

Quantum Relational Hoare Logic with Expectations

Yangjia Li, Dominique Unruh

We present a variant of the quantum relational Hoare logic from (Unruh, POPL 2019) that allows us to use "expectations" in pre- and postconditions. That is, when reasoning about pairs of programs, our logic allows us to quantitatively reason about how much certain pre-/postconditions are satisfied that refer to the relationship between the programs inputs/outputs.

arXiv:1903.08357•Leibniz international proceedings in informatics•Mar 20, 2019•20 citations

Formal Verification of Quantum Algorithms Using Quantum Hoare Logic

Junyi Liu, Bohua Zhan, Shuling Wang +5 more

We formalize the theory of quantum Hoare logic (QHL) [TOPLAS 33(6),19], an extension of Hoare logic for reasoning about quantum programs. In particular, we formalize the syntax and semantics of quantum programs in Isabelle/HOL, write down the rules of quantum Hoare logic, and verify the soundness and completeness of the deduction system for partial correctness of quantum programs. As preliminary work, we formalize some necessary mathematical background in linear algebra, and define tensor products of vectors and matrices on quantum variables. As an application, we verify the correctness of Grover’s search algorithm. To our best knowledge, this is the first time a Hoare logic for quantum programs is formalized in an interactive theorem prover, and used to verify the correctness of a nontrivial quantum algorithm.

Lecture notes in computer science•Jan 1, 2019•83 citations

Hoare Logic for Quantum Programs

Mingsheng Ying

Hoare logic is a foundation of axiomatic semantics of classical programs and it provides effective proof techniques for reasoning about correctness of classical programs. To offer similar techniques for quantum program verification and to build a logical foundation of programming methodology for quantum computers, we develop a full-fledged Hoare logic for both partial and total correctness of quantum programs. It is proved that this logic is (relatively) complete by exploiting the power of weakest preconditions and weakest liberal preconditions for quantum programs.

arXiv:0906.4586•Jun 25, 2009•9 citations

Weakest precondition calculus and relative completeness of satisfaction-based quantum Hoare logic

Xin Sun, Xingchi Su, Xiaoning Bian +1 more

Abstract Quantum Hoare logic (QHL) is a formal verification tool specifically designed to ensure the correctness of quantum programs. There has been an ongoing challenge to achieve a relatively complete satisfaction-based QHL with a while loop since its inception in 2006. This paper presents a solution. We prove the relative completeness in two steps. First, we establish a semantics and proof system of Hoare triples with quantum programs and deterministic assertions. Then, utilizing the weakest precondition of deterministic assertion, we construct the weakest preterm calculus of probabilistic expressions. The relative completeness of QHL is then obtained as a consequence of the weakest preterm calculus.

Quantum Information Processing•Jul 28, 2026•0 citations
We introduce a quantitative relational Hoare logic for quantum programs. Assertions of the logic range over a new infinitary extension of positive semidefinite operators. We prove that our logic is sound, and complete for bounded postconditions and almost surely terminating programs. Our completeness result is based on a quantum version of the duality theorem from optimal transport. We also define a complete embedding into our logic of a relational Hoare logic with projective assertions.
Hoare logic provides a syntax-oriented method to reason about program correctness and has been proven effective in the verification of classical and probabilistic programs. Existing proposals for quantum Hoare logic either lack completeness or support only quantum variables, thus limiting their capability in practical use. In this article, we propose a quantum Hoare logic for a simple while language that involves both classical and quantum variables. Its soundness and relative completeness are proven for both partial and total correctness of quantum programs written in the language. Remarkably, with novel definitions of classical-quantum states and corresponding assertions, the logic system is quite simple and similar to the traditional Hoare logic for classical programs. Furthermore, to simplify reasoning in real applications, auxiliary proof rules are provided that support standard logical operation in the classical part of assertions and super-operator application in the quantum part. Finally, a series of practical quantum algorithms, in particular the whole algorithm of Shor’s factorisation, are formally verified to show the effectiveness of the logic.
We formalize the theory of quantum Hoare logic (QHL) [TOPLAS 33(6),19], an extension of Hoare logic for reasoning about quantum programs. In particular, we formalize the syntax and semantics of quantum programs in Isabelle/HOL, write down the rules of quantum Hoare logic, and verify the soundness and completeness of the deduction system for partial correctness of quantum programs. As preliminary work, we formalize some necessary mathematical background in linear algebra, and define tensor products of vectors and matrices on quantum variables. As an application, we verify the correctness of Grover’s search algorithm. To our best knowledge, this is the first time a Hoare logic for quantum programs is formalized in an interactive theorem prover, and used to verify the correctness of a nontrivial quantum algorithm.
Hoare logic is a foundation of axiomatic semantics of classical programs and it provides effective proof techniques for reasoning about correctness of classical programs. To offer similar techniques for quantum program verification and to build a logical foundation of programming methodology for quantum computers, we develop a full-fledged Hoare logic for both partial and total correctness of quantum programs. It is proved that this logic is (relatively) complete by exploiting the power of weakest preconditions and weakest liberal preconditions for quantum programs.
Abstract Quantum Hoare logic (QHL) is a formal verification tool specifically designed to ensure the correctness of quantum programs. There has been an ongoing challenge to achieve a relatively complete satisfaction-based QHL with a while loop since its inception in 2006. This paper presents a solution. We prove the relative completeness in two steps. First, we establish a semantics and proof system of Hoare triples with quantum programs and deterministic assertions. Then, utilizing the weakest precondition of deterministic assertion, we construct the weakest preterm calculus of probabilistic expressions. The relative completeness of QHL is then obtained as a consequence of the weakest preterm calculus.