Communication-Based Semantics for Recursive Session-Typed Processes

<div>Communicating systems are ubiquitous, and they bring human lives inestimable value.</div><div>Despite this, they often go wrong, sometimes with severe consequences. They are hard to get</div><div>right or reason about because of their inherent complexity. To tame this complexity, we can use</div><div>various formalisms and semantic techniques to model, implement, and reason about communicating</div><div>systems. Notable among these are session-typed programming languages and process calculi.</div><div>Session types [Hon93; HVK98] are a typing discipline for communicating systems. They encode</div><div>communication protocols to specify communications, analogously to how data types specify values</div><div>in functional programs. Importantly, session-typed programming languages guarantee various</div><div>desirable properties of communicating systems.</div><div>Many techniques exist for reasoning about session-typed programming languages and their</div><div>programs.These include linear logical relations [Pér+14; Ton15], game semantics [CY19], denotational</div><div>semantics [Atk17; KMP19], bisimulations [KPY17], and run-time monitoring [GJP18]. Few</div><div>prior approaches have treated inductive and co-inductive session types [Ton15; LM16; DP19] or</div><div>general recursive types [KPY17], or considered higher-order languages that integrate functional</div><div>features and code transmission. Moreover, many prior techniques are not compositional.</div><div>In this dissertation, we present novel semantics and reasoning techniques for Polarized</div><div>SILL [TCP13; PG15], a higher-order session-typed programming language. Polarized SILL coherently</div><div>integrates functional programming with asynchronous session-typed message-passing concurrency.</div><div>It supports recursive communication protocols, value transmission (including code transmission),</div><div>choices (a form of branching), and synchronization. Our contributions are unified by their commitment</div><div>to the process abstraction: communication is the only phenomenon of processes. As a result,</div><div>our semantics define the meaning of processes in terms of their communications. Together, they</div><div>support the following thesis:</div><div>Communication-based semantics elucidate the structure of session-typed languages and</div><div>allow us to reason about programs written in these languages.</div><div>Concretely, we give Polarized SILL three communication-based semantics: an observed communications</div><div>semantics, a communication-based framework for testing equivalences, and a denotational</div><div>semantics.</div><div>Our observed communication semantics defines the meaning of processes to be the communications</div><div>we observe during their executions. Ours is the first to support rich protocols like recursion,</div><div>code transmission, and synchronization.</div><div>We use our observed communication semantics to define extensional notions of program</div><div>equivalence. They are given by a testing equivalences framework. Testing equivalence is a technique</div><div>for defining process equivalence. It deems processes to be equivalent whenever they are indistinguishable</div><div>through experimentation. Classical approaches to testing equivalences [DH84; Hen83; De</div><div>85] define experiment outcomes in terms of states. In contrast, we define experiment outcomes in</div><div>terms of observed communications. We show that one of the testing equivalences captured by our</div><div>framework coincides with barbed congruence, the canonical notion of process equivalence.</div><div>Our denotational semantics defines the meaning of communicating processes to be stable</div><div>continuous functions between dI-domains of session-typed communications. Importantly, our denotational</div><div>semantics is compositional, and we can reason modularly about programs. Our semantics</div><div>is an instance of CYO semantics, a novel kind of semantics that adapts ideas from Kahn semantics for</div><div>dataflow networks [Kah74] to handle bidirectional communications. Our denotational semantics is</div><div>sound relative to barbed congruence.</div><div>To support our work, we make two contributions to the mathematical foundations of programming</div><div>languages semantics. First, we introduce the first notions of fairness for substructural</div><div>operational semantics and multiset rewriting systems, and we study their properties.These fairness</div><div>results are essential to ensuring that our observed communications semantics is well-defined in</div><div>the presence of non-terminating processes. Second, we introduce techniques for reasoning about</div><div>parametrized fixed points of functors, and we study their 2-categorical properties. These results</div><div>underlie our denotational interpretation of recursive session types.</div>