Communication-Based Semantics for Recursive Session-Typed Processes
Creators: name: Kavanagh, Ryan
Publisher: name: Carnegie Mellon University
Year: 2021
Subjects: subject: 80308 Programming Languages
subject: FOS: Computer and information sciences

description: Communicating systems are ubiquitous, and they bring human lives inestimable value.Despite this, they often go wrong, sometimes with severe consequences. They are hard to getright or reason about because of their inherent complexity. To tame this complexity, we can usevarious formalisms and semantic techniques to model, implement, and reason about communicatingsystems. Notable among these are session-typed programming languages and process calculi.Session types [Hon93; HVK98] are a typing discipline for communicating systems. They encodecommunication protocols to specify communications, analogously to how data types specify valuesin functional programs. Importantly, session-typed programming languages guarantee variousdesirable properties of communicating systems.Many techniques exist for reasoning about session-typed programming languages and theirprograms.These include linear logical relations [Pér+14; Ton15], game semantics [CY19], denotationalsemantics [Atk17; KMP19], bisimulations [KPY17], and run-time monitoring [GJP18]. Fewprior approaches have treated inductive and co-inductive session types [Ton15; LM16; DP19] orgeneral recursive types [KPY17], or considered higher-order languages that integrate functionalfeatures and code transmission. Moreover, many prior techniques are not compositional.In this dissertation, we present novel semantics and reasoning techniques for PolarizedSILL [TCP13; PG15], a higher-order session-typed programming language. Polarized SILL coherentlyintegrates functional programming with asynchronous session-typed message-passing concurrency.It supports recursive communication protocols, value transmission (including code transmission),choices (a form of branching), and synchronization. Our contributions are unified by their commitmentto 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. Together, theysupport the following thesis:Communication-based semantics elucidate the structure of session-typed languages andallow us to reason about programs written in these languages.Concretely, we give Polarized SILL three communication-based semantics: an observed communicationssemantics, a communication-based framework for testing equivalences, and a denotationalsemantics.Our observed communication semantics defines the meaning of processes to be the communicationswe observe during their executions. Ours is the first to support rich protocols like recursion,code transmission, and synchronization.We use our observed communication semantics to define extensional notions of programequivalence. They are given by a testing equivalences framework. Testing equivalence is a techniquefor defining process equivalence. It deems processes to be equivalent whenever they are indistinguishablethrough experimentation. Classical approaches to testing equivalences [DH84; Hen83; De85] define experiment outcomes in terms of states. In contrast, we define experiment outcomes interms of observed communications. We show that one of the testing equivalences captured by ourframework coincides with barbed congruence, the canonical notion of process equivalence.Our denotational semantics defines the meaning of communicating processes to be stablecontinuous functions between dI-domains of session-typed communications. Importantly, our denotationalsemantics is compositional, and we can reason modularly about programs. Our semanticsis an instance of CYO semantics, a novel kind of semantics that adapts ideas from Kahn semantics fordataflow networks [Kah74] to handle bidirectional communications. Our denotational semantics issound relative to barbed congruence.To support our work, we make two contributions to the mathematical foundations of programminglanguages semantics. First, we introduce the first notions of fairness for substructuraloperational semantics and multiset rewriting systems, and we study their properties.These fairnessresults are essential to ensuring that our observed communications semantics is well-defined inthe presence of non-terminating processes. Second, we introduce techniques for reasoning aboutparametrized fixed points of functors, and we study their 2-categorical properties. These resultsunderlie our denotational interpretation of recursive session types.