February 1, Urs Schreiber, Topological Quantum Programming via Linear Homotopy Types

[Dan Christensen]

If the weather is cold where you are, you can warm up by attending the
HoTTEST seminar, which resumes this week!

The next talk is on Thursday, February 1 at 11:30am EST (UTC-5) = 16:30 UTC.

Urs Schreiber will be speaking about "Topological Quantum Programming
via Linear Homotopy Types". The talk will be 60 minutes long, followed
by up to 30 minutes of discussion. The abstract is below.

The Zoom link is https://zoom.us/j/994874377

Further information, including the list of upcoming speakers, and
videos and slides from past talks, is available at:

https://www.uwo.ca/math/faculty/kapulkin/seminars/hottest.html

Dan

(On behalf of the HoTTEST organizers: Carlo Angiuli, Dan Christensen,
Chris Kapulkin, and Emily Riehl.)

-----

Urs Schreiber

Topological Quantum Programming via Linear Homotopy Types

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., see
ncatlab.org/schreiber/show/TQC+in+HoTT) 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 Riley's *Linear HoTT*) naturally provides for an
expressive certification-language for quantum programming with
"dynamic lifting" of quantum measurement results (arXiv:2310.15735,
ncatlab.org/schreiber/show/Quantum+Monadology), previously elusive
but arguably necessary for any serious quantum computation.

This is joint work with David J. Myers and Hisham Sati.