WG11/M23Johnson

A quantum computer is a collection of n qubits, which form a basis for a complex vector space of dimension 2^n. A quantum computation can be viewed as a Unitary matrix acting on the qubits. Quantum algorithms correspond to factorizations of unitary matrices into a sequence of gates (often 2x2 or 4x4 unitary matrices). Algorithms can be derived by factoring a given unitary matrix, or a family of matrices, into a product of gates. Alternative factorizations provide algorithmically equivalent choices which can have different costs. In this talk, we derive factorizations of the Discrete Fourier Transform (DFT) matrix into a product of gates and formally verify that the mapping to gates is correct using the Coq proof assistant.