Modern quantum programming languages integrate quantum resources and classical control. They must, on the one hand, be linearly typed to reflect the no-cloning property of quantum resources. On the other hand, high-level and practical languages should also support quantum circuits as first-class citizens, as well as families of circuits that are indexed by some classical parameters. Quantum programming languages thus need linear dependent type theory. This paper defines a general semantic structure for such a type theory via certain fibrations of monoidal categories. The categorical model of the quantum circuit description language Proto-Quipper-M by Rios and Selinger (2017) constitutes an example of such a fibration, which means that the language can readily be integrated with dependent types. We then devise both a general linear dependent type system and a dependently typed extension of Proto-Quipper-M, and provide them with operational semantics as well as a prototype implementation.

• 03B38 - Type theory
• 18M05 - Monoidal categories, symmetric monoidal categories
• 68N15 - Theory of programming languages
• 68N19 - Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)
• 68Q12 - Quantum algorithms and complexity in the theory of computing
• 81P68 - Quantum computation