论文标题
下结构观察到的沟通语义
Substructural Observed Communication Semantics
论文作者
论文摘要
会话类型指定用于通信过程的通信协议，并且通常使用由MultiSet重写系统给出的子结构操作语义指定会话类型的语言。我们为递归的会话类型的语言提供了观察到的通信语义，其中一个过程的观察是由其外部通信给出的。为此，我们介绍了用于多层重写系统的公平执行，并从公平过程执行中提取观察到的通信。这种语义引起了一个直观合理的观察等效概念，即我们猜想与这些语言的语义语义，双音和示意和刺破的一致性相吻合。
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.
