Urs Schreiber: "Effective Quantum Certification via Linear Homotopy Types"

Topos Institute Colloquium, 24th of August 2023.
(Re-uploaded due to a technical issue)
---
The intricacies of realistic - namely: of classically controlled and
(topologically) error-protected - quantum algorithms arguably make
computer-assisted verification a practical necessity; and yet a
satisfactory theory of dependent quantum data types had been missing,
certainly one that would be aware of topological error-protection.
To solve this problem we present Linear homotopy type theory (LHoTT)
as a programming and certification language for quantum computers with
classical control and topologically protected quantum gates, focusing
on (1.) its categorical semantics, which is a homotopy-theoretic
extension of that of Proto-Quipper and a parameterized extension of
Abramsky et al.'s quantum protocols, (2.) its expression of quantum
measurement as a computational effect induced from dependent linear
type formation and reminiscent of Lee at al.‘s dynamic lifting monad
but recovering the interacting systems of Coecke et al.‘s "classical
structures" monads.
Namely, we have recently shown that classical dependent type theory in
its novel but mature full-blown form of Homotopy Type Theory (HoTT) is
naturally a certification language for realistic topological logic
gates. But given that categorical semantics of HoTT is famously
provided by parameterized homotopy theory, we had argued earlier
[Sc14] for a quantum enhancement LHoTT of classical HoTT, now with
semantics in parameterized stable homotopy theory. This linear
homotopy type theory LHoTT has meanwhile been formally described; here
we explain it as the previously missing certified quantum language
with monadic dynamic lifting, as announced in.
Concretely, we observe that besides its support, inherited from HoTT,
for topological logic gates, LHoTT intrinsically provides a system of
monadic computational effects which realize what in algebraic topology
is known as the ambidextrous form of Grothendieck’s “Motivic Yoga”;
and we show how this naturally serves to code quantum circuits subject
to classical control implemented via computational effects. Logically
this emerges as a linearly-typed quantum version of epistemic modal
logic inside LHoTT, which besides providing a philosophically
satisfactory formulation of quantum measurement, makes the language
validate the quantum programming language axioms proposed by Staton;
notably the deferred measurement principle is verified by LHoTT.
Finally we indicate the syntax of a domain-specific programming
language QS (an abbreviation both for “Quantum Systems” and for “QS^0
-modules” aka spectra) which sugars LHoTT to a practical quantum
programming language with all these features; and we showcase
QS-pseudocode for simple forms of key algorithm classes, such as
quantum teleportation, quantum error-correction and
repeat-until-success quantum gates.
(This is joint work with D. J. Myers, M. Riley and H. Sati.
Slides will be available at:
ncatlab.org/schreiber/show/Quantum+Certification+via+Linear+Homotopy+Types)