Imperative Quantum Programming with Ownership and Borrowing in Guppy

TL;DR

The paper addresses the challenge of making imperative quantum programming both ergonomic and safe by introducing a Rust-inspired ownership and borrowing discipline inside Guppy. It distinguishes between owned and borrowed qubits, enforces safe usage through a borrow checker, and prevents leaks and unsafe aliasing, while allowing imperative patterns and integration with classical control. A key contribution is translating imperative Guppy programs into a pure functional intermediate form (HUGR) guided by the ownership discipline, enabling optimization and verification in a functional setting. The work demonstrates practical safety guarantees for imperative quantum code and outlines a concrete path toward formal proofs and broader applicability.

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.