AI 中文总结
研究针对分布式量子系统编程难题，提出Qoreo语言，它以全局编排表达协议，含局部量子语言等。证明编排类型安全，定义端点投影，其元理论机械化，还提供提取管道用于模拟与部署。
AI 中文摘要
编程分布式量子系统需要多个参与者协调量子操作、经典通信和纠缠生成的精确序列。直接将此类协议编写为分布式进程既繁琐又容易出错，细微的不匹配可能导致死锁或产生错误的量子态。我们提出了Qoreo，一种用于量子分布式系统的编排式编程语言，其中整个协议被表示为单个全局程序（编排），而不是独立参与者进程的集合。Qoreo包括一种具有线性类型的局部量子语言，可强化不可克隆原理；一种将局部量子计算与参与者间的经典和量子通信相结合的编排语言；以及用于单个网络节点的进程语言。我们证明了编排的类型安全性，保证类型良好的程序实现定义良好的量子操作，并定义了端点投影（EPP），它能从任何编排自动导出独立进程的网络。我们证明EPP相对于编排语义是健全且完备的；作为推论，每个类型良好的编排都投影到无死锁的进程网络。Qoreo的元理论在Rocq中完全机械化，并且我们提供了一个到NetQASM的提取管道，用于在量子网络硬件上进行模拟和部署。
英文摘要
Programming distributed quantum systems requires multiple actors to coordinate precise sequences of quantum operations, classical communication, and entanglement generation. Writing such protocols directly as distributed processes is tedious and error-prone, and subtle mismatches can cause deadlock or silently incorrect quantum states. We present Qoreo, a choreographic programming language for quantum distributed systems in which an entire protocol is expressed as single, global program (a choreography) rather than as a collection of independent actor processes. Qoreo includes a local quantum language with linear types that enforce the no-cloning principle; a choreographic language that combines local quantum computation with inter-actor classical and quantum communication; and a process language for individual network nodes. We prove type safety for choreographies, guaranteeing that well-typed programs implement well-defined quantum operations, and we define endpoint projection~(EPP), which automatically derives a network of independent processes from any choreography. We prove EPP sound and complete with respect to the choreographic semantics; as a corollary, every well-typed choreography projects to a deadlock-free process network. The metatheory of Qoreo is fully mechanized in Rocq, and we provide an extraction pipeline to NetQASM for simulation and deployment on quantum network hardware.
