Schreiber Topological Quantum Programming in TED-K

Accepted contribution to PlanQC 2022 (for further details see below):



on a scheme for topological quantum programming in terms of twisted equivariant differential K-theory implemented in cohesive homotopy type theory.

Abstract. While the realization of scalable quantum computation will arguably require topological stabilization and, with it, topological-hardware-aware quantum programming and topological-quantum circuit verification, the proper combination of these strategies into dedicated topological quantum programming languages has not yet received attention.

Here we describe a fundamental and natural scheme for typed functional (hence verifiable) topological quantum programming which is fully topological-hardware aware – in that it natively reflects the universal fine technical detail of topological q-bits, namely of symmetry-protected (or enhanced) topologically ordered Laughlin-type anyon ground states in topological phases of quantum materials.

What makes this work is:

  1. our recent result [[SS22-Any, SS22-Ord]] that wavefunctions of realistic and technologically viable anyon species – namely of 𝔰𝔲 ( 2 ) \mathfrak{su}(2) -anyons such as the popular Majorana/Ising anyons but also of computationally universal Fibonacci anyons – are reflected in the twisted equivariant differential (TED) K-cohomology of configuration spaces of codimension=2 nodal defects in the host material’s crystallographic orbifold;

  2. combined with our earlier observation [[SS20-EPB, SS20-Orb, Sc14]] that such TED generalized cohomology theories on orbifolds interpret intuitionistically-dependent linear data types in cohesive homotopy type theory (HoTT), supporting a powerful modern form of modal quantum logic.

Not only should this emulation of anyonic topological hardware functionality via TED-K implemented in cohesive HoTT make advanced formal software verification tools available for hardware-aware topological quantum programming, but the constructive nature of type checking a TED-K quantum program in cohesive HoTT on a classical computer using existing software (such as Agda-\flat), should amount at once to classically simulating the intended quantum computation at the deep level of physical topological q-bits.

This would make TED-K in cohesive HoTT an ideal software laboratory for topological quantum computation on technologically viable types of topological q-bits, complete with ready compilation to topological quantum circuits as soon as the hardware becomes available.

In this short note we give an exposition of the basic ideas, a quick review of the underlying results and a brief indication of the basic language constructs for anyon braiding via TED-K in cohesive HoTT. The language system is under development at the Center for Quantum and Topological Systems at the Research Institute of NYU Abu Dhabi.


Futher details:

The above file is just a brief announcement note. Here are some further details:


  • (1) on the conceptual role of “topological hardware-awareness”

  • (2) technical details of syntax/semantics for topological braid quantum gates




Background results:


Related talks:



Last revised on October 1, 2022 at 14:55:25. See the history of this page for a list of all contributions to it.