Topological Quantum Gates in Homotopy Type Theory

David Jaz Myers, Hisham Sati, Urs Schreiber

Research output: Contribution to journalArticlepeer-review

Abstract

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.

Original languageEnglish (US)
Article number172
JournalCommunications In Mathematical Physics
Volume405
Issue number7
DOIs
StatePublished - Jul 2024

ASJC Scopus subject areas

  • Statistical and Nonlinear Physics
  • Mathematical Physics

Fingerprint

Dive into the research topics of 'Topological Quantum Gates in Homotopy Type Theory'. Together they form a unique fingerprint.

Cite this