Message-Observing Sessions

TL;DR

Most introduces a trace-based, binding-aware framework for message-observing session types, enabling protocols to depend on messages observed across ambient channels. It extends binary session types with type-level processes to express global invariants, and develops a two-phase typechecking approach anchored in a semantic relation between process traces and specification traces. The core contributions are the semantic foundation with traces and bindings, a compositional typing discipline, and proofs of safety and compositionality, alongside extensible directions such as selection, asynchrony, value-dependence, and recursion. This work advances precise guarantees about complex, interdependent communications and provides a foundation toward a robust type theory for session-based concurrency.

Abstract

We present Most, a process language with message-observing session types. Message-observing session types extend binary session types with type-level computation to specify communication protocols that vary based on messages observed on other channels. Hence, Most allows us to express global invariants about processes, rather than just local invariants, in a bottom-up, compositional way. We give Most a semantic foundation using traces with binding, a semantic approach for compositionally reasoning about traces in the presence of name generation. We use this semantics to prove type soundness and compositionality for Most processes. We see this as a significant step towards capturing message-dependencies and providing more precise guarantees about processes.

Figures (3)

• Figure 1: Uniform Process Typing Judgment
• Figure 2: Right-Focussed Process Typing --- Focussed Type in Weak Head Normal Form
• Figure 3: Right-Focussed Process Typing --- Reducing the Type in Focus