一句话：提出 facet 记法，为可受控共享状态的 actor 语言提供理论、类型系统与行为类型系统，并报告实现经验。
Actor 语言通常以消息传递实现并发，使用简单，但实际代码表明程序员偶尔需要让 actor 与其他 actor 共享部分状态。dataspace 模型为此在 actor 模型上加入一种严格受控的状态交换机制；然而经验显示，这种共享要求语言提供能表达 actor 会话时序方面的构造。本文提出 facet 记法，围绕共享状态 actor 的编程与推理给出其理论、类型系统与行为类型系统，并报告初步实现经验。facet 旨在让程序员描述 actor 状态共享的时间结构，并使相关程序性质可被类型化地推理。评估主要是理论构建与首轮实现体验，而非大规模实证。
Abstract Actor languages realize concurrency via message passing, which most of the time is easy to use. Empirical code inspection provides evidence, however, that on occasion, programmers wish to have an actor share some of its state with others. The dataspace model adds a tightly controlled state-exchange mechanism, dubbed dataspace, to the actor model for just this purpose. Experience with dataspaces suggests that this form of sharing calls for linguistic constructs that allow programmers to state temporal aspects of actor conversations. In response, this paper presents the facet notation: its theory, its type system, its behavioral type system, and some first experiences with an implementation.
@article{paperbot2682,
title = {Programming and reasoning about actors that share state},
author = {SAM CALDWELL and TONY GARNOCK-JONES and MATTHIAS FELLEISEN},
journal = {Journal of Functional Programming},
volume = {34},
year = {2024},
doi = {10.1017/s0956796824000091}
}