通信量子进程

论文信息（2005，POPL，pp. 145–157）：Simon J. Gay、Rajagopal Nagarajan。DOI；arXiv:quant-ph/0409052；作者版本

工作

本文提出 CQP（Communicating Quantum Processes），用于建模同时包含量子通信、经典通信和计算的系统。CQP 把 pi 演算的通信原语与测量、量子态变换结合起来，允许 qubit 沿通信信道在进程之间传递。论文定义语法、操作语义和静态类型系统，并用类型保存性与唯一所有权性质约束并发系统中的量子资源。

主要贡献

• 把进程演算的通信机制扩展到量子比特和量子操作。
• 用通道类型区分经典与量子数据，并控制量子态的使用。
• 证明操作语义保持类型，且每个 qubit 在系统中由唯一进程拥有。
• 用若干量子通信系统示例说明 CQP 可作为形式分析和验证的基础。

局限与适用范围

CQP 的所有权安全是静态资源性质，不等于通信协议已经满足保密性、功能正确性或容错要求。论文的操作语义是理想化模型，不直接描述硬件噪声、网络延迟、编译开销或设备连接。并发系统的完整验证仍需要额外的逻辑、等价关系和证明工具。

与其他工作的关系

CQP 把 QPL 语言 与 带经典控制的量子 Lambda 演算 的语言和类型问题推进到并发通信场景。它与 量子协议的范畴语义 都关注协议组合，但 CQP 以进程、信道和操作语义为中心；与后续量子进程代数和协议验证工作相比，它突出唯一所有权这一静态不变量。

原论文

Simon J. Gay and Rajagopal Nagarajan, Communicating Quantum Processes, in POPL 2005, pp. 145–157, DOI: 10.1145/1040305.1040318. 作者版本