The Logic of Quantum Programs

TL;DR

This paper introduces a dynamic logic framework for reasoning about information flow, entanglement, and quantum operations in quantum programs, providing a formal method for analyzing quantum protocols like teleportation.

Contribution

It develops a logical calculus with syntax and semantics to analyze quantum information flow, entanglement, and transformations, including a sound proof system and applications to quantum protocols.

Findings

Logical calculus for quantum information flow

Characterization of entanglement and operators through logic

Analysis of quantum teleportation protocol

Abstract

We present a logical calculus for reasoning about information flow in quantum programs. In particular we introduce a dynamic logic that is capable of dealing with quantum measurements, unitary evolutions and entanglements in compound quantum systems. We give a syntax and a relational semantics in which we abstract away from phases and probabilities. We present a sound proof system for this logic, and we show how to characterize by logical means various forms of entanglement (e.g. the Bell states) and various linear operators. As an example we sketch an analysis of the teleportation protocol.