An article that we have written:
David Jaz Myers, $\;$ Hisham Sati $\,$ and $\,$ Urs Schreiber:
Topological Quantum Gates in Homotopy Type Theory
Comm. Math. Phys. 405 172 (2024)
doi:10.1007/s00220-024-05020-8
download:
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 (elusive) physical realization as well as their quantum information-theoretic nature. Building on recent results on defect branes in string/M-theory [SS23a] and on their holographically dual anyonic defects in condensed matter theory [SS23b], here we explain (as announced in [SS22]) 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 the 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 a companion article (announced earlier) 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 into verified quantum circuits with quantum measurement gates and classical control.
Companion articles:
Expository talks:
Topological Quantum Programming via Linear Homotopy Types
presentation at Quantum Physics and Logic (QPL 2024), Buenes Aires, 15 July 2024
Topological Quantum Gates in HoTT
talk at QFT and Cobordism 2023,
NYU Abu Dhabi, March 2023
video: YT
Topological Quantum Programming via Linear Homotopy Types
talk at: Homotopy Type Theory Electronic Seminar,
01 Feb 2024
video: YT
Abstract. It is interesting to observe that a use-case of what deserves to be called genuine “homotopical computation” is secretly known: We showed in arXiv:2303.02382 (in print at Comm. Math. Phys) that the specification of the logic gates envisioned in “topological quantum computation on anyons”, while intricate in traditional language, have a slick expression in HoTT, simply as transport of certain truncated dependent function types into Eilenberg-MacLane types. The mathematical theorems behind this are a remarkable result on conformal quantum field theory by Feigin, Schechtmann & Varchenko (1994) combined with our novel algebro-topological construction, lending itself to formalization in HoTT, of Gauss-Manin connections on fibrations of twisted cohomology groups.
Generally, the relation between HoTT and quantum computation is closer than might be suspected: Adding rules meant to enforce interpretation of HoTT into infinity-topoi of parameterized module spectra (such as in Riley‘s Linear HoTT) naturally provides for an expressive certification-language for quantum programming with “dynamic lifting” of quantum measurement results (arXiv:2310.15735), previously elusive but arguably necessary for any serious quantum computation.
This is joint work with David J. Myers and Hisham Sati.
Script:
Gauss-Manin connections on twisted cohomology in traditional literature. | p. 231 in Voisin | |
Gauss-Manin connection on twisted cohomology as dependent function type transport. | p. 69 in TQG | |
Configuration spaces, braid groups and their finite presentations. | pp. 13 in TQG | |
KZ-connection on $\mathfrak{su}(2)$-anyonic conformal blocks as dependent function type transport. | p. 76 in TQG | |
Identified via FSV94‘s hypergeometric integral-construction of Laughlin wavefunctions. | p. 32 in Ord | |
The quantum adiabatic theorem and topological quantum gates. | p. 21 in TQG | |
Need for certified topological quantum language. | pp. 3 in Tow | |
A case for linear homotopy type theory. | pp. 3 in QM | |
Quantum modalities from dependent linear types. | pp. 69 in QM | |
(Deferred) Quantum measurement from Quantum modalities. | pp. 78 in QM | |
Doubly monoidal model category for dependent linearly-typed topological quantum gates. | pp. 1 in EoS |
Related articles:
Topological Quantum Programming in TED-K
PlanQC 2022 33 (2022)
[arXiv:2209.08331, video presentation: YT]
Anyonic defect branes in TED-K-theory
Rev. Math. Phys. (2023)
Anyonic topological order in TED K-theory
Rev. Math. Phys. (2023)
Related talks:
Towards Certified Topological Quantum Programming via Linear Homotopy Types,
talk at Quantum Information and Quantum Matter 2024,
NYU Abu Dhabi, 27-31 May 2024
Towards Quantum Programming via Linear Homotopy Types,
talk at Homotopy Type Theory and Computing – Classical and Quantum,
CQTS @ New York University Abu Dhabi, 19-21 April 2024
Topological Quantum Programming via Linear Homotopy Types
talk at: Homotopy Type Theory Electronic Seminar (01 Feb 2024)
Towards verified topological hardware-aware quantum programming
slides: pdf (view on full screen)
talk at CQTS & TII Workshop 2023
NYU Abu Dhabi, 24 Feb 2023
TED K-theory of Cohomotopy moduli spaces and Anyonic Topological Order
talk at Higher Structures and Field Theory,
ESI Vienna, 25 Aug 2022
Quantum Data Types via Linear Homotopy Type Theory
talk at Workshop on Quantum Software @ QTML 2022
Naples, 12 Nov 2022
slides: pdf (view on full screen)
Topological Quantum Gates from M-Theory
talk at M-Theory and Mathematics 2023
NYU Abu Dhabi, Jan 2023
Effective Quantum Certification via Linear Homotopy Types,
talk at Colloquium of the Topos Institute,
Part I: 13 April 2023, Part II: 24 Aug 2023
Last revised on July 16, 2024 at 00:04:52. See the history of this page for a list of all contributions to it.