QWIRE：量子线路核心语言

论文信息（2017，POPL）：Jennifer Paykin、Robert Rand、Steve Zdancewic。DOI；论文条目

工作

QWIRE 是用于定义量子线路、并把线路嵌入任意经典宿主语言的核心语言。它只有少量原语，却通过宿主语言获得模块化和表达能力，体现 QRAM 模型中经典计算机控制量子线路的结构。论文给出类型系统、操作语义和基于密度矩阵的指称语义，并讨论宿主语言安全时的安全性与强正规化。

主要贡献

• 提出一个最小而可嵌入宿主语言的量子线路核心。
• 给出类型系统与操作语义，并证明相应安全性质。
• 用密度矩阵定义线路的指称语义。
• 展示通用分析框架和依赖类型等宿主语言扩展。

局限与适用范围

QWIRE 的安全和强正规化结论依赖宿主语言及其假设；核心语言本身不解决所有硬件编译、噪声、资源成本或高层算法证明问题。密度矩阵语义描述理想线路行为，不能替代具体后端校准和执行验证。

与其他工作的关系

QWIRE 将 线性类型系统 和 量子线路 结合成可嵌入的核心语言，可与 Quipper 的可扩展线路生成对照。它也延续 QPL 与 带经典控制的量子 Lambda 演算 的类型化语义方向，但把重点放在线路对象和宿主语言接口。

原论文

Jennifer Paykin, Robert Rand, and Steve Zdancewic, QWIRE: A Core Language for Quantum Circuits, in POPL 2017. DOI: 10.1145/3009837.3009894. 论文条目