A project that we are developing at CQTS:
David J. Myers, $\;$ Mitchell Riley, $\;$ Hisham Sati, $\;$ Urs Schreiber:
Effective Quantum Certification via Linear Homotopy Types
extended abstract: pdf
Abstract. 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 [MSS23] 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 theoryLHoTT
has meanwhile been formally described [Ri22]; here we explain it as the previously missing certified quantum language with monadic dynamic lifting, as announced in [Sc22].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 [St14]; 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 “$Q S^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.
Companion articles:
A Linear Dependent Type Theory with Identity Types
as a Quantum Verification Language
(translation between
LHoTT
and the proto-Quipper
of Fu, Kishida & Selinger 2020)
David Jaz Myers, Hisham Sati, Urs Schreiber:
Topological Quantum Gates in Homotopy Type Theory
(certification of topological quantum gates in
HoTT
)
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.
Effective Quantum Certification via Linear Homotopy Types,
talk at Colloquium of the Topos Institute
Part I: 13 April 2023
video: YT
slides: pdf (view full screen)
(upcoming) Part II: 17 Aug 2023
slides: pdf (view full screen)
Related talks:
Topological Quantum Programming in TED-K
talk at PlanQC 2022 33 (15 Sep 2022)
Precursor discussion:
Last revised on May 17, 2023 at 11:45:53. See the history of this page for a list of all contributions to it.