Ryan Kavanagh

Communication-Based Semantics for Recursive Session-Typed Processes Degree Type: Ph.D. in Computer Science
Advisor(s): Stephen Brookes, Frank Pfenning
Graduated: December 2021

Abstract:

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 get right or reason about because of their inherent complexity. To tame this complexity, we can use various formalisms and semantic techniques to model, implement, and reason about communicating systems. Notable among these are session-typed programming languages and process calculi. Session types [Hon93; HVK98] are a typing discipline for communicating systems. They encode communication protocols to specify communications, analogously to how data types specify values in functional programs. Importantly, session-typed programming languages guarantee various desirable properties of communicating systems.

Many techniques exist for reasoning about session-typed programming languages and their programs. These include linear logical relations [Pér+14; Ton15], game semantics [CY19], denotational semantics [Atk17; KMP19], bisimulations [KPY17], and run-time monitoring [GJP18]. Few prior approaches have treated inductive and co-inductive session types [Ton15; LM16; DP19] or general recursive types [KPY17], or considered higher-order languages that integrate functional features and code transmission. Moreover, many prior techniques are not compositional.

In this dissertation, we present novel semantics and reasoning techniques for Polarized SILL [TCP13; PG15], a higher-order session-typed programming language. Polarized SILL coherently integrates 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 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. Together, they support the following thesis:

Communication-based semantics elucidate the structure of session-typed languages and allow us to reason about programs written in these languages.

Concretely, we give Polarized SILL three communication-based semantics: an observed communications semantics, a communication-based framework for testing equivalences, and a denotational semantics.

Our observed communication semantics 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.

We use our observed communication semantics to define extensional notions of program equivalence. They are given by a testing equivalences framework. Testing equivalence is a technique for defining process equivalence. It deems processes to be equivalent whenever they are indistinguishable through experimentation. Classical approaches to testing equivalences [DH84; Hen83; De85] define experiment outcomes in terms of states. In contrast, we define experiment outcomes in terms of observed communications. We show that one of the testing equivalences captured by our framework coincides with barbed congruence, the canonical notion of process equivalence.

Our denotational semantics defines the meaning of communicating processes to be stable continuous functions between dI-domains of session-typed communications. Importantly, our denotational semantics is compositional, and we can reason modularly about programs. Our semantics is an instance of CYO semantics, a novel kind of semantics that adapts ideas from Kahn semantics for dataflow networks [Kah74] to handle bidirectional communications. Our denotational semantics is sound relative to barbed congruence.

To support our work, we make two contributions to the mathematical foundations of programming languages semantics. First, we introduce the first notions of fairness for substructural operational semantics and multiset rewriting systems, and we study their properties. These fairness results are essential to ensuring that our observed communications semantics is well-defined in the presence of non-terminating processes. Second, we introduce techniques for reasoning about parametrized fixed points of functors, and we study their 2-categorical properties. These results underlie our denotational interpretation of recursive session types.

Thesis Committee:
Stephen Brookes (Co-Chair)
Frank Pfenning (Co-Chair)
Jan Hoffmann
Luís Caires (Universidade Nova de Lisboa)
Gordon Plotkin (University of Edinburgh)

Srinivasan Seshan, Head, Computer Science Department
Martial Hebert, Dean, School of Computer Science

Keywords:
Session types, program equivalence, general recursion, observed communication semantics, testing equivalence, denotational semantics