Topological Quantum Gates in Homotopy Type Theory

Despite the plausible necessity of topological protection for realizing scalable quantum computers, the conceptual underpinnings of topological quantum logic gates had arguably remained shaky, both regarding their physical realization as well as their information-theoretic nature. Building on recent results on defect branes in string/M-theory (Sati and Schreiber in Rev Math Phys, 2023. https://doi.org/10.1142/S0129055X23500095. [arXiv:2203.11838]) and on their holographically dual anyonic defects in condensed matter theory (Sati and Schreiber in Rev Math Phys 35(03):2350001, 2023. https://doi.org/10.1142/S0129055X23500010. [arXiv:2206.13563]), here we explain [as announced in Sati and Schreiber (PlanQC 2022:33, 2022, [arXiv:2209.08331], [ncatlab.org/schreiber/show/Topological+Quantum+Programming+in+TED-K])] how the specification of realistic topological quantum gates, operating by anyon defect braiding in topologically ordered quantum materials, has a surprisingly slick formulation in parameterized point-set topology, which is so fundamental that it lends itself to certification in modern homotopically typed programming languages, such as cubical Agda. We propose that this remarkable confluence of concepts may jointly kickstart the development of topological quantum programming proper as well as of real-world application of homotopy type theory, both of which have arguably been falling behind their high expectations; in any case, it provides a powerful paradigm for simulating and verifying topological quantum computing architectures with high-level certification languages aware of the actual physical principles of realistic topological quantum hardware. In companion articles (Sati and Schreiber in The Quantum Monadology, [arXiv:2310.15735], Sati and Schreiber in Entanglement of Sections: The pushout of entangled and parameterized quantum information [arXiv:2309.07245]) [announced in Schreiber (Quantum types via Linear Homotopy Type Theory, talk at Workshop on Quantum Software @ QTML2022, Naples, 2022, [ncatlab.org/schreiber/files/QuantumDataInLHoTT-221117.pdf])], we explain how further passage to “dependent linear” homotopy types naturally extends this scheme to a full-blown quantum programming/certification language in which our topological quantum gates may be compiled to verified quantum circuits, complete with quantum measurement gates and classical control.