Communication-Based Semantics for Recursive Session-Typed Processes
Communicating systems are ubiquitous, but they are hard to get right. Fortunately, we can use session-typed programming languages to help us correctly implement communicating systems.
In this thesis, we present novel semantics and reasoning techniques for Polarized SILL, a higher-order session-typed programming language. Polarized SILL coherently integrates functional programming with asynchronous message-passing concurrency. It also supports recursive communication protocols, code transmission, and synchronization.
Our contributions are unified by their commitment to the process abstraction: communication is the only phenomenon of processes. As a result, our semantics define the meaning of processes in terms of their communications. Concretely, we give Polarized SILL three communication- based semantics:
An observed communication semantics. It defines the meaning of processes to be the communications we observe during their executions. Ours is the first to support rich protocols like recursion, code transmission, and synchronization.
A communication-based testing equivalences framework. It deems processes to be equivalent whenever they are indistinguishable through experimentation. One of our testing equivalences coincides with barbed congruence, the canonical notion of process equivalence.
A denotational semantics. It defines the meaning of communicating processes to be stable continuous functions between dI-domains of session-typed communications. It adapts ideas from Kahn semantics for dataflow networks to handle bidirectional communications, and it is sound relative to barbed congruence. Importantly, it lets us reason modularly about programs.
We illustrate our techniques by applying them to several case studies.