Abstract

The Game Semantics of Reachability Types

The presence of shared (i.e. aliased) mutable state has long been recognised as the root cause of many difficulties in programming, particularly complicating understanding and reasoning about the behaviour of programs. Approaches to controlling aliasing are a rich area of study and have become increasingly adopted in mainstream programming languages. Reachability Types are a recent approach to provide control over sharing in a higher-order functional programming language, by tracking in the type system information about what resources are reachable from a term, which allows separation requirements to be enforced using types.

In this talk, I will discuss applying operational game semantics (OGS) to investigate the meaning of reachability types and the impact these have on a language. We will be concerned with capturing contextual equivalence (and approximation), a well-studied notion in programming language theory exposing what can be observed about terms from within the language. The restrictions reachability types impose lead to some subtle equivalences. In particular, the language is not observably sequential.

Following the OGS paradigm, I will start by presenting a simple model based upon a labelled transition system generating traces that soundly capture the interaction between a term and all possible contexts. By identifying properties that these traces satisfy, I will show how we can develop a series of improved models. Ultimately, by introducing a notion of reordering on traces to handle the lack of observable sequentiality, we will arrive at the first fully abstract model of a language with reachability types. This model can be further simplified to ground it in a nominal version of Mazurkiewicz traces.

This talk is based on my DPhil thesis, with the major results having appeared in preliminary form in the 2025 LICS Paper ‘Reachability Types, Traces, and Full Abstraction’, co-authored with my supervisor, Andrzej Murawski.