Communication-Based Semantics for Recursive Session-Typed Processes

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; De

85] 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.