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:


Related talks:





Last revised on December 20, 2022 at 10:30:19. See the history of this page for a list of all contributions to it.