Fairness and communication-based semantics for session-typed languages
Polarized SILL is a programming language that combines functional programming with session-typed message-passing concurrency. It features general recursion; code and channel transmission; and synchronous and asynchronous communication. To reason about Polarized SILL programs, we develop the first program equivalence framework based on observable communications.
We give meaning to Polarized SILL programs using an observed communication semantics (OCS). Our OCS is the first to support general recursion and code transmission. We then develop a communication-based testing equivalences framework and show that one of the equivalences captured by our framework coincides with barbed congruence, the canonical notion of process equivalence.
Polarized SILL’s operational semantics is specified using a multiset rewriting system. We introduce fairness for multiset rewriting systems to ensure that our OCS is well-defined in the presence of non-terminating processes, and use fairness properties to simplify reasoning about processes.
This work lays the foundation for observational reasoning for session-typed languages with general recursion.