Reachability types, traces and full abstraction

Journal article

Reachability types are a recent approach to modelling sharing in higher-order languages, aiming to provide separation guarantees through typability. The contextual equivalence problem in such a setting is exacerbated by the need to consider reachability-related constraints on the allowable interactions. In particular, they might weaken the ability of contexts to observe sequentiality.

In this paper, we investigate contextual equivalence for reachability types through the lens of operational game semantics. We provide a sound trace model for a language equipped with reachability types, and show how to refine it to a fully abstract one, which captures a natural notion of equivalence based on allowing terms to share functions and locations consistently with the assigned reachability annotations. We also discuss the corresponding problem of contextual approximation, along with an inequational full abstraction result.

This is a first attempt at defining a fully abstract semantics for reachability types.

Authors: Bunting, B; Murawski, AS

• Peer review status: Peer reviewed
• Publisher: IEEE
• Acceptance date: 2025-04-08
• Event title: 40th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2025)
• Event location: Singapore
• Event website: https://lics.siglog.org/lics25/
• Event start date: 2025-06-23
• Event end date: 2025-06-26
• Language: English
• Keywords: reachability types; game semantics; trace models; full abstraction