The Game Semantics of Reachability Types

This project falls into the EPSRC Programming Languages and Compilers research area.
Modern programming languages are increasingly providing features to give programmers more control over aliasing. Aliasing arises when two variables in a program refer to the same underlying object or location. The presence of unconstrained aliasing complicates reasoning about programs, as verifying local properties can require global knowledge to establish what the impact of operations, and can be the source of subtle bugs. Controlling aliasing can eliminate these issues and also makes it easier for languages to provide automated features.
An example is Rust, a high-performance systems programming language designed to allow both low-level interaction with hardware, while providing memory safety, which ensures compiled programs do not crash. Memory safe languages often incorporate a feature called a garbage collection, which runs alongside the user's program to free unused memory. This, unsurprisingly, leads to poor performance, and so Rust avoids this by having an advanced typing system which tracks who 'owns' values in the program, so they can be identified as unused. Rust achieves this through a principle called aliasing-xor-mutability, where objects have a unique owner, and can only be shared if they are not able to be updated, through a system of borrows. Rust has proven the utility of controlling aliasing, and has been successfully adopted by industry.
Investigating how to control aliasing, and what impact this has on the resulting programming language, are thus interesting research questions. One approach to this is through Reachability Types. These are a recently proposed system to investigate combining control over aliasing with features of higher-order functional programming. This is done by annotating types to indicate what variables are reachable from a term of that type, and then providing restrictions by limiting the overlap of annotations. It can be used to encode patterns such as the borrows found in Rust. What the meaning of these reachability types are has not yet been fully explored.
The key objective of this project is to understand the semantics of the reachability types through the lens of game semantics. The semantics of a programming language gives a mathematical meaning to programs written in that language. Game semantics is a style based on the idea that a part of a program (a term) can be modelled as a strategy in a game of question and answer it plays with its environment. Over the last 25 years, game semantics has proven to be a powerful paradigm, providing results for languages with many diverse features. This project will investigate how the presence of reachability types manifests itself in the strategies of terms.
One key question which drives semantic investigations is that of contextual equivalence - essentially asking if one term can be substituted for another everywhere. Determining if terms are contextually equivalent is useful in tasks like verifying compiler optimisations. Adding constraints on aliasing limits what different parts of a program can observe about a term, so has a big impact on contextual equivalence, which a semantic model can illuminate. With a semantic model in hand, we can consider investigate developing reasoning techniques for programs using reachability types. Techniques exploiting game semantics have produced automatic methods for program verification in other settings, and so it is hoped the same will be the case here. The presence of additional constraints poses both challenges and opportunities - as they have to be enforced on contexts, but limit the behaviour of terms that have to be considered.
As reachability types are intended to provide a foundational language for investigating aliasing, it can be hoped that the techniques and ideas developed might be transferable to other languages which seek to control aliasing.