一句话：提出首个带类型且支持一等进程名与位置集合多态的编排式语言 λQC，并在 Rocq 中验证其无死锁性。
编排式编程让开发者编写单一集中式程序，再编译为各节点程序，但现有编排式语言缺乏现代系统所需的关键特性，例如节点动态计算应由谁执行并把决定告知其他节点。本文提出 λQC，这是首个带类型的一等进程名编排式语言，支持对类型和位置集合的多态，并支持代数与递归数据类型以及多重定位值，从而提升表达力。作者在 Rocq 中形式化并机器验证主要结果，包括编排式编程标准的无死锁保证。
Choreographic programming is a promising new paradigm for programming concurrent systems where a developer writes a single centralized program that compiles to individual programs for each node. Existing choreographic languages, however, lack critical features integral to modern systems, like the ability of one node to dynamically compute who should perform a computation and send that decision to others. This work addresses this gap with λ QC, the first typed choreographic language with first class process names and polymorphism over both types and (sets of) locations. λ QC also improves expressive power over previous work by supporting algebraic and recursive data types as well as multiply-located values. We formalize and mechanically verify our results in Rocq, including the standard choreographic guarantee of deadlock freedom.
@article{paperbot3008,
title = {Choreographic Quick Changes: First-Class Location (Set) Polymorphism},
author = {Ashley Samuelson and Andrew K. Hirsch and Ethan Cecchetti},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA2},
year = {2025},
doi = {10.1145/3763114}
}