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.

Mathematical Foundations

• Predicates : Definition and properties of stabilizer predicates.

• Normalization : Functions and lemmas for 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.

• Examples : A collection of verified programs.

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.