Department of

September 2019 October 2019 November 2019 Su Mo Tu We Th Fr Sa Su Mo Tu We Th Fr Sa Su Mo Tu We Th Fr Sa 1 2 3 4 5 6 7 1 2 3 4 5 1 2 8 9 10 11 12 13 14 6 7 8 9 10 11 12 3 4 5 6 7 8 9 15 16 17 18 19 20 21 13 14 15 16 17 18 19 10 11 12 13 14 15 16 22 23 24 25 26 27 28 20 21 22 23 24 25 26 17 18 19 20 21 22 23 29 30 27 28 29 30 31 24 25 26 27 28 29 30

Tuesday, October 8, 2019

**Abstract:** Desirable features of a quantum programming language include: treating both quantum resources and classical control; being a functional language admitting semantics and other formal methods; and dependent types. The type theory of such a language must be linear to reflect the linearity of quantum processes, and we want it to involve parameters (values that are known at circuit generation time) and states (values known at circuit execution time) to describe and generate quantum circuits. The goal of this talk is to provide a general semantic structure for linear dependent type theory of that sort. We review categorical models of quantum processes and the sets-and-functions model of classical dependent type theory, and show how they can be integrated to model linear dependent type theory of classical parameters and quantum states. This is joint work with Frank Fu, Julien Ross, and Peter Selinger.