一句话：提出 Qurts，用带生命周期的仿射类型统一实现量子程序自动反计算。
量子程序中的反计算允许丢弃值而不丢失量子信息，并使编译器复用资源。量子信息通常必须由类型系统线性处理，而自动反计算则要求亚结构类型系统介于线性与仿射之间；已有语言对此支持较为临时。本文提出 Qurts：将 Rust 类型系统扩展到量子场景，通过用生命周期参数化类型，使其在生命周期内可仿射使用、在生命周期外受线性限制，从而为自动反计算提供统一框架。作者还给出两种操作语义：一种基于经典模拟，另一种不依赖具体反计算策略。摘要未报告实现或实验评估。
Uncomputation is a feature in quantum programming that allows the programmer to discard a value without losing quantum information, and that allows the compiler to reuse resources. Whereas quantum information has to be treated linearly by the type system, automatic uncomputation enables the programmer to treat it affinely to some extent. Automatic uncomputation requires a substructural type system between linear and affine, a subtlety that has only been captured by existing languages in an ad hoc way. We extend the Rust type system to the quantum setting to give a uniform framework for automatic uncomputation called Qurts (pronounced quartz). Specifically, we parameterise types by lifetimes, permitting them to be affine during their lifetime, while being restricted to linear use outside their lifetime. We also provide two operational semantics: one based on classical simulation, and one that does not depend on any specific uncomputation strategy.
@article{paperbot3247,
title = {Qurts: Automatic Quantum Uncomputation by Affine Types with Lifetime},
author = {Kengo Hirata and Chris Heunen},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {POPL},
year = {2025},
doi = {10.1145/3704842}
}