DROPS

Document

DOI: 10.4230/LIPIcs.CONCUR.2026.45

Concurrent Visibility: Higher-Order Concurrency with First-Order Store

Authors: Iwan Quémerais, Guilhème Jaber, Ken Sakayori, and Davide Sangiorgi

Published in: LIPIcs, Volume 391, 37th International Conference on Concurrency Theory (CONCUR 2026)

Abstract

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.

Cite as

Iwan Quémerais, Guilhème Jaber, Ken Sakayori, and Davide Sangiorgi. Concurrent Visibility: Higher-Order Concurrency with First-Order Store. In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 45:1-45:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{quemerais_et_al:LIPIcs.CONCUR.2026.45,
  author =	{Qu\'{e}merais, Iwan and Jaber, Guilh\`{e}me and Sakayori, Ken and Sangiorgi, Davide},
  title =	{{Concurrent Visibility: Higher-Order Concurrency with First-Order Store}},
  booktitle =	{37th International Conference on Concurrency Theory (CONCUR 2026)},
  pages =	{45:1--45:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-447-5},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{391},
  editor =	{Sokolova, Ana and Totzke, Patrick},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2026.45},
  URN =		{urn:nbn:de:0030-drops-273760},
  doi =		{10.4230/LIPIcs.CONCUR.2026.45},
  annote =	{Keywords: Operational game semantics, higher-order effectful programs, mutable store}
}

Search Results

Documents authored by Jaber, Guilhème

Concurrent Visibility: Higher-Order Concurrency with First-Order Store

Abstract

Cite as

Thanks for your feedback!

Could not send message