2026-08-25T22:09:01Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:27376 2026-08-24T14:08:32Z ddc:004 open_access

Concurrent Visibility: Higher-Order Concurrency with First-Order Store Quémerais, Iwan Jaber, Guilhème Sakayori, Ken Sangiorgi, Davide Operational game semantics higher-order effectful programs mutable store We propose an Operational Game Semantics for a (call-by-value) concurrent higher-order language with first-order store (references may contain other references or first-order values such as integers or booleans; however they may not store higher-order values such as functions). We adapt the game-semantic notion of visibility, which semantically captures the absence of higher-order references and developed for sequential higher-order languages, to a concurrent setting. We thus define a complete-trace preorder, and prove it sound for the contextual preorder, by introducing a synchronization-based composition of semantic configurations and establishing an observational adequacy result. We also prove completeness for the subset of the language in which functions return first-order values. In contrast to the case of sequential visibility, in the labeled transition semantics we have to account for the presence of multiple active threads with possibly different visibilities, and of a tree-like structure for managing the dependencies among the threads so created. Moreover, we have to reason on families of traces, rather than single traces, as in concurrent setting the order among certain actions cannot be enforced. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Iwan Quémerais and Guilhème Jaber and Ken Sakayori and Davide Sangiorgi 2026 Is Part Of LIPIcs, Volume 391, 37th International Conference on Concurrency Theory (CONCUR 2026) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CONCUR.2026.45 urn:nbn:de:0030-drops-273760 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2026.45 eng https://creativecommons.org/licenses/by/4.0/legalcode