BEGIN:VCALENDAR VERSION:2.0 PRODID:researchseminars.org CALSCALE:GREGORIAN X-WR-CALNAME:researchseminars.org BEGIN:VEVENT SUMMARY:Urs Schreiber DTSTART:20230413T170000Z DTEND:20230413T180000Z DTSTAMP:20260403T195821Z UID:ToposInstituteColloquium/87 DESCRIPTION:Title: Effective Quantum Certification via Linear Homotopy Type s\nby Urs Schreiber as part of Topos Institute Colloquium\n\n\nAbstrac t\nThe intricacies of realistic — namely: of classically controlled and (topologically) error-protected — quantum algorithms arguably make compu ter-assisted verification a practical necessity\; and yet a satisfactory t heory of dependent quantum data types had been missing\, certainly one tha t would be aware of topological error-protection.\n\nTo solve this problem we present Linear homotopy type theory (LHoTT) as a programming and certi fication language for quantum computers with classical control and topolog ically protected quantum gates\, focusing on (1.) its categorical semantic s\, 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 li fting monad but recovering the interacting systems of Coecke et al.'s "cla ssical structures" monads.\n\nNamely\, we have recently shown that classic al dependent type theory in its novel but mature full-blown form of Homoto py Type Theory (HoTT) is naturally a certification language for realistic topological logic gates. But given that categorical semantics of HoTT is f amously provided by parameterized homotopy theory\, we had argued earlier [Sc14] for a quantum enhancement LHoTT of classical HoTT\, now with semant ics in parameterized stable homotopy theory. This linear homotopy type the ory LHoTT has meanwhile been formally described\; here we explain it as th e previously missing certified quantum language with monadic dynamic lifti ng\, as announced in.\n\nConcretely\, 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 a lgebraic topology is known as the ambidextrous form of Grothendieck’s "M otivic Yoga"\; and we show how this naturally serves to code quantum circu its subject to classical control implemented via computational effects. Lo gically this emerges as a linearly-typed quantum version of epistemic moda l logic inside LHoTT\, which besides providing a philosophically satisfact ory formulation of quantum measurement\, makes the language validate the q uantum programming language axioms proposed by Staton\; notably the deferr ed measurement principle is verified by LHoTT.\n\nFinally 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 LH oTT 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.\n\n(This is joint work with D. J. Myers\, M. Riley and H. Sati. Slides will be available at: ncatlab.org/schreiber/show/Quant um+Certification+via+Linear+Homotopy+Types)\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/87/ END:VEVENT END:VCALENDAR