A Theorem Prover for Quantum Hoare Logic and Its Applications

Understand

Quantum Hoare Logic (QHL) was introduced in Ying's work to specify and reason about quantum programs.

• In this paper, we implement a theorem prover for QHL based on Isabelle/HOL.
• By applying the theorem prover, verifying a quantum program against a specification is transformed equivalently into an order relation between matrices.
• Due to the limitation of Isabelle/HOL, the calculation of the order relation is solved by calling an outside oracle written in Python.