Substructural Observed Communication Semantics

TL;DR

This paper introduces an observed communication semantics for session-typed languages with recursion, using fair executions in multiset rewriting systems to analyze external communications and define observational equivalence.

Contribution

It proposes a novel observed semantics based on fair executions, bridging operational and semantic equivalences for session-typed languages with recursion.

Findings

Defines fair executions for multiset rewriting systems

Extracts observed communications from process executions

Proposes a new notion of observational equivalence

Abstract

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.