POPL 2026
Sun 11 - Sat 17 January 2026 Rennes, France

Quantum data cannot in general be copied or deleted, forcing it to be treated differently to classical data, and often preventing the use of classical programming language abstractions in a quantum setting. Within the setting of functional quantum programming languages, this property is often captured by linear typing, ensuring that any quantum data must be consumed exactly once. However, many mainstream quantum toolkits adopt an imperative style, where variables are understood to represent mutable references to quantum data. In this abstract, we discuss how the linearity translates to this setting, arguing that safe use of quantum data corresponds to preventing shared ownership of mutable references. We further demonstrate that this restricted mutability allows programs to defined concisely, and further facilitates convenient constructions which appear unnatural in the functional setting. Finally, we present a type system for enforcing single ownership of quantum registers which can be sliced and indexed, which can be checked efficiently and produces informative localised errors.

Extended Abstract (planqc26-paper20.pdf)338KiB