Effective Quantum Certification via Linear Homotopy Types

Watch a technical colloquium talk from the Topos Institute that explores Linear Homotopy Type Theory (LHoTT) as a programming and certification language for quantum computers with classical control and topologically protected quantum gates. Delve into the categorical semantics of LHoTT, examining its homotopy-theoretic extension of Proto-Quipper and parameterized extension of quantum protocols. Learn how quantum measurement is expressed as a computational effect through dependent linear type formation, and understand its connection to dynamic lifting monad and classical structures monads. Explore how LHoTT serves as a certification language for realistic topological logic gates, providing monadic computational effects that implement classical control in quantum circuits. Discover the practical applications through QS programming language examples, including quantum teleportation, quantum error-correction, and repeat-until-success quantum gates.