Schreiber Topological Quantum Programming in Linear Homotopy Type Theory

An article that we are writing at CQTS:

---

• Topological Quantum Programming

  in Linear Homotopy Type Theory

introducing linear homotopy type theory as a natural general-purpose quantum programming language inside which is naturally embedded:

1. QS – a domain specific programming language for quantum circuits of quantum logic gates with classical control & effects;

2. TED-K – a domain specific programming language for topologically ordered topological phases of matter, and specifically of anyon braid quantum gates in topological quantum computation.

---

For more see the extended abstract: Topological Quantum Programming in TED-K and Topological Quantum Gates in Homotopy Type Theory.

Expository presentations:

• 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)

  $\,$

  Abstract. The proper concept of data types in quantum programming languages, hence of their formal verification and categorical semantics, has remained somewhat elusive, as witnessed by the issue of “dynamic lifting” encountered in the Quipper language family. In this talk I explain our claim that a powerful quantum data type-system elegantly solving these problems is naturally provided by the linear homotopy type theory recently realized by M. Riley. Together with our previous claim that homotopy type theory natively knows about the fine detail of $\mathfrak{su}$(2)-anyon braid quantum gates, this shows that linear homotopy type theory is a natural substrate for typed quantum programming languages aware of topological quantum hardware.

  This is joint work, at CQTS, with D. J. Myers, M. Riley and Hisham Sati.

Related talks:

• Topological Quantum Programming in TED-K

  talk at PlanQC 2022 33 (15 Sep 2022)

  [talk slides: pdf, video: YT]

---