Ross Duncan - Verifying Quantum Computations with the ZX-calculus

Real implementations of quantum algorithms on real quantum devices are not going to resemble the nice circuit drawings we find in Nielsen and Chuang. To actually run a quantum program we are going to need to translate from some simple high-level description, like a circuit diagram, to a complicated low-level description taking into account all the error correction, the quirks of the qubits, the architectural constraints of the machine etc etc etc. How can we have confidence that the final program is equivalent to the original one? One possible answer is to use the ZX-calculus. The ZX-calculus is (a) a formal axiomatic system based on the theory of monoidal categories; (b) a graphical tensor notation which is universal for quantum computation; and (c) a simple and effective way for reasoning about quantum systems which is suitable for automation. In this talk I’ll introduce the ZX-calculus and give two examples of its use, one related to MBQC and the other related to QECC.