带经典控制的量子计算 Lambda 演算
A Lambda Calculus for Quantum Computation with Classical Control
Selinger 与 Valiron 用带仿射线性类型的 Lambda 演算表达量子数据、经典控制和安全性。
论文信息（TLCA 2005，LNCS 3461，pp. 354–368；MSCS 扩展版 2006）：Peter Selinger、Benoît Valiron。会议 DOI；期刊 DOI；arXiv:cs/0404056
工作
本文把简单类型 Lambda 演算扩展为一种量子函数式语言，遵循“quantum data, classical control”范式。它给出 call-by-value 操作语义，用仿射直觉线性逻辑设计类型系统，并讨论量子类型和量子操作如何在函数式程序中组合。论文的主要理论结果包括语言的安全性性质和类型推断算法。
主要贡献
- 给出带量子类型与量子操作的函数式语言设计。
- 用 call-by-value 操作语义明确程序执行和测量的控制方式。
- 用仿射线性逻辑限制量子资源的重复使用，同时允许适当丢弃。
- 建立安全性结果并给出类型推断算法的设计。
局限与适用范围
这是语言、类型和语义层面的研究，不是面向特定硬件的完整编译器。仿射类型保证资源使用纪律，但不自动证明算法后置条件、测量概率、终止性或噪声下的行为。高阶量子计算、动态资源和现实设备约束需要更丰富的语义与实现模型。
与其他工作的关系
它是 QPL 语言 类型化和经典控制路线的函数式延伸，也与 QML 共享线性资源与范畴语义动机。它相较于 van Tonder 的 量子 Lambda 演算 更明确地给出经典控制、操作语义和类型推断；这些语言设计又可与 通信量子进程 的并发通信模型对照。
原论文
Peter Selinger and Benoît Valiron, A Lambda Calculus for Quantum Computation with Classical Control, TLCA 2005, LNCS 3461, 354–368 (2005), expanded in Mathematical Structures in Computer Science 16(3), 527–552 (2006), conference DOI: 10.1007/11417170_26, journal DOI: 10.1017/S0960129506005238. arXiv:cs/0404056