BEGIN:VCALENDAR VERSION:2.0 PRODID:researchseminars.org CALSCALE:GREGORIAN X-WR-CALNAME:researchseminars.org BEGIN:VEVENT SUMMARY:Urs Schreiber DTSTART:20230824T170000Z DTEND:20230824T180000Z DTSTAMP:20260403T200056Z UID:ToposInstituteColloquium/104 DESCRIPTION:Title: Quantum Programming via Linear Homotopy Types\nby U rs Schreiber as part of Topos Institute Colloquium\n\n\nAbstract\nThe intr icacies of realistic — namely: of classically controlled and\n(topologic ally) error-protected — quantum algorithms arguably make\ncomputer-assis ted verification a practical necessity\; and yet a\nsatisfactory theory of dependent quantum data types had been missing\,\ncertainly one that would be aware of topological error-protection.\n\nTo solve this problem we pre sent Linear homotopy type theory (LHoTT)\nas a programming and certificati on language for quantum computers with\nclassical control and topologicall y protected quantum gates\, focusing\non (1.) its categorical semantics\, which is a homotopy-theoretic\nextension of that of Proto-Quipper and a pa rameterized extension of\nAbramsky et al.'s quantum protocols\, (2.) its e xpression of quantum\nmeasurement as a computational effect induced from d ependent linear\ntype formation and reminiscent of Lee at al.‘s dynamic lifting monad\nbut recovering the interacting systems of Coecke et al.‘s "classical\nstructures" monads.\n\nNamely\, we have recently shown that c lassical dependent type theory in\nits novel but mature full-blown form of Homotopy Type Theory (HoTT) is\nnaturally a certification language for re alistic topological logic\ngates. But given that categorical semantics of HoTT is famously\nprovided by parameterized homotopy theory\, we had argue d earlier\n[Sc14] for a quantum enhancement LHoTT of classical HoTT\, now with\nsemantics in parameterized stable homotopy theory. This linear\nhomo topy type theory LHoTT has meanwhile been formally described\; here\nwe ex plain it as the previously missing certified quantum language\nwith monadi c dynamic lifting\, as announced in.\n\nConcretely\, we observe that besid es its support\, inherited from HoTT\,\nfor topological logic gates\, LHoT T intrinsically provides a system of\nmonadic computational effects which realize what in algebraic topology\nis known as the ambidextrous form of G rothendieck’s “Motivic Yoga”\;\nand we show how this naturally serve s to code quantum circuits subject\nto classical control implemented via c omputational effects. Logically\nthis emerges as a linearly-typed quantum version of epistemic modal\nlogic inside LHoTT\, which besides providing a philosophically\nsatisfactory formulation of quantum measurement\, makes the language\nvalidate the quantum programming language axioms proposed by Staton\;\nnotably the deferred measurement principle is verified by LHoTT .\n\nFinally we indicate the syntax of a domain-specific programming\nlang uage QS (an abbreviation both for “Quantum Systems” and for “QS^0\n- modules” aka spectra) which sugars LHoTT to a practical quantum\nprogram ming language with all these features\; and we showcase\nQS-pseudocode for simple forms of key algorithm classes\, such as\nquantum teleportation\, quantum error-correction and\nrepeat-until-success quantum gates.\n\n(This is joint work with D. J. Myers\, M. Riley and H. Sati.\nSlides will be av ailable at:\nncatlab.org/schreiber/show/Quantum+Certification+via+Linear+H omotopy+Types)\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/104/ END:VEVENT END:VCALENDAR