一句话：提出 whole-spectrum implementation 可实现性概念与类型系统，刻画编排中非确定选择如何由确定性实现完整实现。
编排通过消息传递规定多方交互，其实现由独立进程组合而成。已有正确性/完备性关系多假设选择是非确定的，难以对应实际语言中的确定性条件分支。本文提出 whole-spectrum implementation（全谱实现）这一可实现性概念：编排层仍保留非确定选择，而实现层将选择确定性化，并排除某些角色实现无论置于何种上下文都永不采用某一分支的情形。作者给出类型规则以检查全谱实现，并说明该概念如何精确刻画编排与实现之间的关系。最后以 POP 协议为案例进行分析。
Choreographies specify multiparty interactions via message passing. A realisation of a choreography is a composition of independent processes that behave as specified by the choreography. Existing relations of correctness/completeness between choreographies and realisations are based on models where choices are non-deterministic. Resolving non-deterministic choices into deterministic choices (e.g., conditional statements) is necessary to correctly characterise the relationship between choreographies and their implementations with concrete programming languages. We introduce a notion of realisability for choreographies - called whole-spectrum implementation - where choices are still non-deterministic in choreographies, but are deterministic in their implementations. Our notion of whole spectrum implementation rules out deterministic implementations of roles that, no matter which context they are placed in, will never follow one of the branches of a non-deterministic choice. We give a type discipline for checking whole-spectrum implementations. As a case study, we analyse the POP protocol under the lens of whole-spectrum implementation.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{BocchiMT20,
title = {On Resolving Non-determinism in Choreographies},
author = {Laura Bocchi and Hernan Melgratti and Emilio Tuosto},
journal = {Logical Methods in Computer Science},
volume = {Volume 16, Issue 3},
year = {2020},
doi = {10.23638/lmcs-16(3:18)2020}
}