Categorical Quantum Logic and the ZX-Calculus

My final project for CSC 747: Introduction to Quantum Computing, which outlines the basic semantics of the ZX-calculus and then uses it to diagramatically study a few simple quantum circuits. Noteworthy applications include proving the correctness of GHZ preparation, deriving a compositional invariant of the Pauli circuit, and formally verifying the quantum teleportation algorithm.