Linear Dependent Type Theory for Quantum Programming Languages

Abstract

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.

References in corpus (6)

• Linear Haskell: practical linearity in a higher-order polymorphic language
• An Introduction to Quantum Programming in Quipper
• QWIRE Practice: Formal Verification of Quantum Circuits in Coq
• Framed bicategories and monoidal fibrations
• A tutorial introduction to quantum circuit programming in dependently typed Proto-Quipper
• A Biset-Enriched Categorical Model for Proto-Quipper with Dynamic Lifting

Cited by in corpus (6)

• A tutorial introduction to quantum circuit programming in dependently typed Proto-Quipper
• Formal Methods for Quantum Programs: A Survey
• Polynomial Time and Dependent Types
• Quantum Hoare Type Theory
• Hybrid dynamical type theories for navigation
• Encoding High-level Quantum Programs as SZX-diagrams