Reachability types, traces and full abstraction

Conference item

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 reach-ability 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

• Publication status: Published
• Peer review status: Peer reviewed
• Publisher: IEEE
• Host title: 2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
• Pages: 527-540
• Publication date: 2025-06-23
• 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
• DOI: 10.1109/LICS65433.2025.00046
• EISBN: 9798331579005
• ISBN: 9798331579012
• Language: English
• Keywords: trace models; full abstraction; game semantics; reachability types