A Type-Theoretic Account of Quantum Computation
Offered By: ACM SIGPLAN via YouTube
Course Description
Overview
Explore a type-theoretic approach to quantum computation in this 28-minute conference talk from ACM SIGPLAN's TyDe'23. Delve into the presentation by Takafumi Saikawa and Jacques Garrigue as they use type-theoretic concepts to describe and prove properties of quantum computations, with a focus on quantum circuits. Discover how the speakers combine several components represented using dependent and polymorphic types in Coq, including lenses, finite functions, currying, polymorphism, and subtypes. Gain insights into their comprehensive account of pure quantum circuits and learn about the process of proving properties from the ground up in this extended abstract presentation.
Syllabus
[TyDe'23] A type-theoretic account of quantum computation (Extended Abstract)
Taught by
ACM SIGPLAN
Related Courses
Introduction to programming with dependent types in ScalaStepik On Voevodsky's Univalence Principle - André Joyal
Institute for Advanced Study via YouTube Univalent Foundations and the Equivalence Principle - Benedikt Ahrens
Institute for Advanced Study via YouTube A Little Taste of Dependent Types
Strange Loop Conference via YouTube Dependent Types in Haskell
Strange Loop Conference via YouTube