# Schreiber Topological Quantum Programming in TED-K (Rev #10, changes)

Showing changes from revision #9 to #10: Added | Removed | Changed

A brief announcement note that we are finalizing (for further details see below):

• Hisham Sati, $\;$ Urs Schreiber:

\linebreak

Topological Quantum Computation in TED-K

\linebreak

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 $\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.

\linebreak

Futher details:

\linebreak

\linebreak

Background results:

\linebreak

Revision on June 25, 2022 at 06:12:27 by Urs Schreiber. See the history of this page for a list of all contributions to it.