Title: A Categorical Semantics for Linear and Quantum Dependent Type Theory
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. If time permits, I will also discuss how to incorporate
features such as the one called dynamic lifting. This talk is based on
joint work with Frank Fu, Julien Ross, and Peter Selinger.