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.