子结构观察通信语义
Substructural Observed Communication Semantics
摘要：
会话类型为通信进程指定通信协议，并且会话类型语言通常使用由多集重写系统给出的子结构操作语义来指定。我们为具有递归的会话类型语言给出了一个观察到的通信语义，其中进程的观察是通过其外部通信给出的。要做到这一点，我们引入公平执行多集重写系统，并提取公平的进程执行观察到的通信。这种语义诱导了一个直观合理的概念，观察等价，我们猜想符合语义等价引起的指称语义，互模拟，倒钩同余这些语言。
英文摘要：
Session-types specify communication protocols for communicating processes, and session-typed languages are often specified using substructural operational semantics given by multiset rewriting systems. We give an observed communication semantics for a session-typed language with recursion, where a process's observation is given by its external communications. To do so, we introduce fair executions for multiset rewriting systems, and extract observed communications from fair process executions. This semantics induces an intuitively reasonable notion of observational equivalence that we conjecture coincides with semantic equivalences induced by denotational semantics, bisimulations, and barbed congruences for these languages.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
