一句话：提出 Proto-Quipper-R，用线性依赖类型与效应系统推导电路宽度参数上界，并实现 QuRA 工具验证。
量子电路描述语言虽可用经典高层语言编写量子算法，但其生成的电路可能远超当前量子硬件的量子比特与门资源。本文提出 Proto-Quipper-R，一种带线性依赖类型-效应系统的电路描述语言，能为程序产生的电路宽度推导参数化上界。作者证明了类型安全性，并证明其资源分析相对于大步操作语义是正确的。最后实现静态分析工具 QuRA，用于 QFT 和 Grover 算法等真实量子算法，展示可自动验证电路宽度。
Circuit description languages are a class of quantum programming languages in which programs are classical and produce a description of a quantum computation, in the form of a quantum circuit . Since these programs can leverage all the expressive power of high-level classical languages, circuit description languages have been successfully used to describe complex quantum algorithms, whose circuits, however, may involve many more qubits and gate applications than current quantum architectures can actually muster. In this article, we present Proto-Quipper-R , a circuit description language endowed with a linear dependent type-and-effect system capable of deriving parametric upper bounds on the width of the circuits produced by a program. We prove both the standard type safety results and that the resulting resource analysis is correct with respect to a big-step operational semantics. Lastly, we introduce QuRA , a static analysis tool based on Proto-Quipper-R ’s type system, and use it to show that our framework allows for the automatic width verification of realistic quantum algorithms, such as the QFT and Grover’s algorithm.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{ColledanL24,
title = {Circuit Width Estimation via Effect Typing and Linear Dependency},
author = {Andrea Colledan and Ugo Dal Lago and Niki Vazou},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {47},
number = {3},
year = {2025},
doi = {10.1145/3737282}
}