一句话：为 Proto-Quipper 演算提出基于单子的指称模型，分离值与电路副作用，并支持电路资源分析。
论文研究 Quipper 及其理想化演算 Proto-Quipper 家族的语义基础。作者引入基于索引单子的指称模型，将项所归约到的值与项作为副作用生成的电路分离，从而可对生成电路的大小等资源性质进行指称解释与验证。进一步提出 circuit algebra 这一新概念，用以刻画电路组合与优化，并据此给出效应类型系统，保证最终电路满足定量性质，即使在优化后仍成立。该工作为量子电路描述语言提供了统一的指称语义与资源分析框架。
In this paper, a monad-based denotational model is introduced and shown adequate for the Proto-Quipper family of calculi, themselves being idealized versions of the Quipper programming language. The use of a monadic approach allows us to separate the value to which a term reduces from the circuit that the term itself produces as a side effect. In turn, this enables the denotational interpretation and validation of rich type systems in which the size of the produced circuit can be controlled. Notably, the proposed semantic framework, through the novel concept of circuit algebra, suggests forms of effect typing guaranteeing quantitative properties about the resulting circuit, even in presence of optimizations.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2511-22419,
title = {On Circuit Description Languages, Indexed Monads, and Resource Analysis},
author = {Ken Sakayori and Andrea Colledan and Ugo Dal Lago},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {POPL},
year = {2026},
doi = {10.1145/3776666}
}