BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Reachability Types\, Traces\, and Full Abstraction - Benedict Bunt
 ing (University of Cambridge)
DTSTART:20260424T130000Z
DTEND:20260424T140000Z
UID:TALK246704@talks.cam.ac.uk
CONTACT:Ioannis Markakis
DESCRIPTION:<p><em style="background-color: rgb(255\, 255\, 255)\; color: 
 rgb(0\, 0\, 0)\;">The Game Semantics of Reachability Types</em></p><p><spa
 n style="background-color: rgb(255\, 255\, 255)\; color: rgb(0\, 0\, 0)\;"
 >The presence of shared (i.e. </span><em style="background-color: rgb(255\
 , 255\, 255)\; color: rgb(0\, 0\, 0)\;">aliased</em><span style="backgroun
 d-color: rgb(255\, 255\, 255)\; color: rgb(0\, 0\, 0)\;">) mutable state h
 as long been recognised as the root cause of many difficulties in programm
 ing\, particularly complicating understanding and reasoning about the beha
 viour of programs. Approaches to controlling aliasing are a rich area of s
 tudy and have become increasingly adopted in mainstream programming langua
 ges. </span><em style="background-color: rgb(255\, 255\, 255)\; color: rgb
 (0\, 0\, 0)\;">Reachability Types</em><span style="background-color: rgb(2
 55\, 255\, 255)\; color: rgb(0\, 0\, 0)\;"> are a recent approach to provi
 de control over sharing in a higher-order functional programming language\
 , by tracking in the type system information about what resources are reac
 hable from a term\, which allows separation requirements to be enforced us
 ing types.</span></p><p><span style="background-color: rgb(255\, 255\, 255
 )\; color: rgb(0\, 0\, 0)\;"> </span></p><p><span style="background-color:
  rgb(255\, 255\, 255)\; color: rgb(0\, 0\, 0)\;">In this talk\, I will dis
 cuss applying </span><em style="background-color: rgb(255\, 255\, 255)\; c
 olor: rgb(0\, 0\, 0)\;">operational game semantics (OGS)</em><span style="
 background-color: rgb(255\, 255\, 255)\; color: rgb(0\, 0\, 0)\;"> to inve
 stigate the meaning of reachability types and the impact these have on a l
 anguage. We will be concerned with capturing </span><em style="background-
 color: rgb(255\, 255\, 255)\; color: rgb(0\, 0\, 0)\;">contextual equivale
 nce </em><span style="background-color: rgb(255\, 255\, 255)\; color: rgb(
 0\, 0\, 0)\;">(and approximation)\, a well-studied notion in programming l
 anguage theory exposing what can be observed about terms from within the l
 anguage. The restrictions reachability types impose lead to some subtle eq
 uivalences. In particular\, the language is not </span><em style="backgrou
 nd-color: rgb(255\, 255\, 255)\; color: rgb(0\, 0\, 0)\;">observably seque
 ntial.</em></p><p><span style="background-color: rgb(255\, 255\, 255)\; co
 lor: rgb(0\, 0\, 0)\;"> </span></p><p><span style="background-color: rgb(2
 55\, 255\, 255)\; color: rgb(0\, 0\, 0)\;">Following the OGS paradigm\, I 
 will start by presenting a simple model based upon a labelled transition s
 ystem generating traces that soundly capture the interaction between a ter
 m and all possible contexts. By identifying properties that these traces s
 atisfy\, I will show how we can develop a series of improved models. Ultim
 ately\, by introducing a notion of </span><em style="background-color: rgb
 (255\, 255\, 255)\; color: rgb(0\, 0\, 0)\;">reordering</em><span style="b
 ackground-color: rgb(255\, 255\, 255)\; color: rgb(0\, 0\, 0)\;"> on trace
 s to handle the lack of observable sequentiality\, we will arrive at the f
 irst </span><em style="background-color: rgb(255\, 255\, 255)\; color: rgb
 (0\, 0\, 0)\;">fully abstract</em><span style="background-color: rgb(255\,
  255\, 255)\; color: rgb(0\, 0\, 0)\;"> model of a language with reachabil
 ity types. This model can be further simplified to ground it in a nominal 
 version of Mazurkiewicz traces.</span></p><p><span style="background-color
 : rgb(255\, 255\, 255)\; color: rgb(0\, 0\, 0)\;"> </span></p><p><span sty
 le="background-color: rgb(255\, 255\, 255)\; color: rgb(0\, 0\, 0)\;">This
  talk is based on my DPhil thesis\, with the major results having appeared
  in preliminary form in the 2025 LICS Paper ‘</span><em style="backgroun
 d-color: rgb(255\, 255\, 255)\; color: rgb(0\, 0\, 0)\;">Reachability Type
 s\, Traces\, and Full Abstraction’\,</em><span style="background-color: 
 rgb(255\, 255\, 255)\; color: rgb(0\, 0\, 0)\;"> co-authored with my super
 visor\, Andrzej Murawski.</span></p>
LOCATION:SS03\, Computer Laboratory
END:VEVENT
END:VCALENDAR