Proof rules for purely quantum programs

TL;DR

This paper develops proof rules and semantics for analyzing purely quantum programs, enabling formal reasoning about quantum algorithms within a specific quantum computing architecture.

Contribution

It introduces denotational and weakest precondition semantics for a quantum language fragment and extends classical proof rules to quantum loops.

Findings

Semantics for quantum language fragment established

Proof rules extended to quantum loops

Framework supports formal verification of quantum programs

Abstract

We apply the notion of quantum predicate proposed by D'Hondt and Panangaden to analyze a purely quantum language fragment which describes the quantum part of a future quantum computer in Knill's architecture. The denotational semantics, weakest precondition semantics, and weakest liberal precondition semantics of this language fragment are introduced. To help reasoning about quantum programs involving quantum loops, we extend proof rules for classical probabilistic programs to our purely quantum programs.