舞蹈动作的快速变化：一类定位（集合）多态性

《Proceedings of the ACM on Programming Languages》：Choreographic Quick Changes: First-Class Location (Set) Polymorphism

λQC是新型编舞语言，支持第一类过程名称、类型与位置多态性，解决动态计算与通信问题，提供代数递归数据类型和多地点值，并通过Rocq形式化验证保证无死锁。

　　

摘要

编舞编程是一种用于并发系统编程的有前景的新范式，开发者编写一个集中的程序，该程序会被编译成每个节点的单独程序。然而，现有的编舞语言缺乏现代系统所必需的关键特性，例如某个节点能够动态判断谁应该执行某个计算，并将这一决策发送给其他节点。本研究通过 λ_QC 来填补这一空白。λ_QC 是第一种支持“一类进程名称”以及对类型和（集合）位置进行多态化的类型化编舞语言。它还通过支持代数和递归数据类型以及多位置值，提升了编程的表达能力。我们在 Rocq 框架中对我们的结果进行了形式化定义和机械验证，包括标准的编舞编程保证——即无死锁特性。