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.
An imperative update to the Guppy programming language from Quantinuum presented by Mark Koch at a talk at PLanQC 2025 co-located with POPL ‘25.