一句话：为 Quipper 设计基于效应与细化类型的类型系统，自动推导电路宽度、深度、门数等资源上界。
论文针对量子电路描述语言中难以静态预估电路资源的问题，为 Quipper 提出一个类型系统，用于推导类型化程序所生成电路规模的上界。其核心是效应与细化类型，二者都依赖 index，即通用算术表达式；这些表达式的运算符可根据目标度量采用不同解释，从而统一支持宽度、深度、门数以及仅统计特定线型或门种类的变体。作者通过逻辑谓词证明该方法的正确性，并在对资源度量的合理假设下给出可靠性保证。实现方面，QuRA 工具进行了实证评估，结果表明在许多情况下可以全自动推断出紧致上界。
We introduce a type system for the Quipper language designed to derive upper bounds on the size of the circuits produced by the typed program. This size can be measured according to various metrics, including width , depth and gate count , but also variations thereof obtained by considering only some wire types or some gate kinds. The key ingredients for achieving this level of flexibility are effects and refinement types, both relying on indices , that is, generic arithmetic expressions whose operators are interpreted differently depending on the target metric. The approach is shown to be correct through logical predicates, under reasonable assumptions about the chosen resource metric. This approach is empirically evaluated through the QuRA tool, showing that, in many cases, inferring tight bounds is possible in a fully automatic way.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{ColledanL25,
title = {Flexible Type-Based Resource Estimation in Quantum Circuit Description Languages},
author = {Andrea Colledan and Ugo Dal Lago},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {POPL},
year = {2025},
doi = {10.1145/3704883}
}