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.

翻译：线性类型在函数式量子编程中强制执行不可克隆与不可删除定理。然而，在命令式量子编程领域，此类类型系统尚未获得广泛应用。本研究致力于开发一种量子类型系统，该体系将符合人体工程学的线性类型机制与命令式语义相结合，同时保持安全性保证。本文提出的所有理念均已实现于Quantinuum公司的Guppy编程语言中。