Heisenberg-Foundations

The basics of the Heisenberg representation of quantum computing

Mathematical Foundations

• Preamble : Mathematical definitions and lemmas.

• LinAlg : Result about linear algebra.

• F2Math : Math on the finite field of characteristic 2.

Hoare-Heisenberg Logic

• Predicates : Definition and properties of stabilizer predicates.

• Normalization : Functions and lemmas for normalization.

• PivotRule : Additional definitions and properties of normalization.

• HoareHeisenbergLogic : Main file that contains the core logic of Hoare-Heisenberg Logic.

• Separability : Definition and lemmas about separability.

• Automation : Definitions and tactics for automation.

• ReflexiveAutomation : A more efficient enhanced automation.

• Measurement : Definitions, lemmas, and tactics about classical control and measurement, with an example of the Steane quantum error correcting circuit.

• examples_and_benchmarks : A collection of examples and benchmarks.

This project is based on Hoare meets Heisenberg: A Lightweight Logic for Quantum Programs by Aarthi Sundaram, Robert Rand, Kartik Singhal, and Brad Lackey.

This repository depends on the external library QuantumLib (https://github.com/inQWIRE/QuantumLib).

This repository was developed and tested for Coq 8.19.2.