Imperative Quantum Programming with Ownership and Borrowing in Guppy

Abstract

Linear types enforce no-cloning and no-deleting theorems in functional quantum programming. However, in imperative quantum programming, they have not gained widespread adoption. This work aims to develop a quantum type system that combines ergonomic linear typing with imperative semantics and maintains safety guarantees. All ideas presented here have been implemented in Quantinuum's Guppy programming language.

Presented at the Fifth International Workshop on Programming Languages for Quantum Computing (PLanQC 2025)