Document Open Access Logo

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

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

PDF

File

Thumbnail PDF
PDF
LIPIcs.CONCUR.2026.45.pdf
  • Filesize: 0.94 MB
  • 20 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Program semantics
Keywords
  • Operational game semantics
  • higher-order effectful programs
  • mutable store

Metrics

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 Get BibTex

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) https://doi.org/10.4230/LIPIcs.CONCUR.2026.45

Author Details

Iwan Quémerais
  • ENS de Lyon & University of Bologna, Italy
Guilhème Jaber
  • Nantes Université, France
Ken Sakayori
  • The University of Tokyo, Japan
Davide Sangiorgi
  • University of Bologna & INRIA, Italy

Funding

  • Sakayori, Ken: JSPS KAKENHI Grant Number JP24K20731.

References

  1. Samson Abramsky, Radha Jagadeesan, and Pasquale Malacaria. Full abstraction for PCF. Inf. Comput., 163(2):409-470, 2000. URL: https://doi.org/10.1006/INCO.2000.2930.
  2. Samson Abramsky and Guy McCusker. Linearity, sharing and state: a fully abstract game semantics for idealized algol with active expressions. In Jean-Yves Girard, Mitsuhiro Okada, and Andre Scedrov, editors, Linear Logic Tokyo Meeting 1996, Keio University, Mita Campus, Tokyo, Japan, March 29 - April 2, 1996, Electronic Notes in Theoretical Computer Science, pages 2-14. Elsevier, 1996. URL: https://doi.org/10.1016/S1571-0661(05)80398-6.
  3. Dariusz Biernacki, Sergueï Lenglet, and Piotr Polesiuk. A complete normal-form bisimilarity for state. In Mikolaj Bojanczyk and Alex Simpson, editors, Foundations of Software Science and Computation Structures - 22nd International Conference, FOSSACS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Lecture Notes in Computer Science, pages 98-114. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-17127-8_6.
  4. Lars Birkedal, Filip Sieczkowski, and Jacob Thamsborg. A concurrent logical relation. In Patrick Cégielski and Arnaud Durand, editors, Computer Science Logic - 26th International Workshop / 21st Annual Conference of the EACSL, CSL 2012, Fontainebleau, France, September 3-6, 2012, volume 16 of LIPIcs, pages 107-121. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012. URL: https://doi.org/10.4230/LIPIcs.CSL.2012.107.
  5. Peio Borthelle, Tom Hirschowitz, Guilhem Jaber, and Yannick Zakowski. An abstract, certified account of operational game semantics. In Viktor Vafeiadis, editor, Programming Languages and Systems - 34th European Symposium on Programming, ESOP 2025, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025, Hamilton, ON, Canada, May 3-8, 2025, Proceedings, Part I, Lecture Notes in Computer Science, pages 172-199. Springer, 2025. URL: https://doi.org/10.1007/978-3-031-91118-7_7.
  6. Simon Castellan and Pierre Clairambault. Disentangling parallelism and interference in game semantics. Log. Methods Comput. Sci., 20(3), 2024. URL: https://doi.org/10.46298/LMCS-20(3:24)2024.
  7. Simon Castellan, Pierre Clairambault, and Glynn Winskel. Thin games with symmetry and concurrent Hyland-Ong games. Log. Methods Comput. Sci., 15(1), 2019. URL: https://doi.org/10.23638/LMCS-15(1:18)2019.
  8. Derek Dreyer, Georg Neis, and Lars Birkedal. The impact of higher-order state and control effects on local relational reasoning. J. Funct. Program., 22(4-5):477-528, 2012. URL: https://doi.org/10.1017/S095679681200024X.
  9. Dan R. Ghica and Andrzej S. Murawski. Angelic semantics of fine-grained concurrency. Ann. Pure Appl. Log., 151(2-3):89-114, 2008. URL: https://doi.org/10.1016/J.APAL.2007.10.005.
  10. Daniel Hirschkoff, Iwan Quémerais, and Davide Sangiorgi. First-order store and visibility in name-passing calculi. In Patricia Bouyer and Jaco van de Pol, editors, 36th International Conference on Concurrency Theory, CONCUR 2025, Aarhus, Denmark, August 26-29, 2025, LIPIcs, pages 23:1-23:21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2025.23.
  11. Furio Honsell, Ian A Mason, Scott Smith, and Carolyn Talcott. A variable typed logic of effects. Information and computation, 119(1):55-90, 1995. URL: https://doi.org/10.1006/INCO.1995.1077.
  12. Chung-Kil Hur, Derek Dreyer, Georg Neis, and Viktor Vafeiadis. The marriage of bisimulations and kripke logical relations. In John Field and Michael Hicks, editors, Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, Philadelphia, Pennsylvania, USA, January 22-28, 2012, pages 59-72. ACM, 2012. URL: https://doi.org/10.1145/2103656.2103666.
  13. J. M. E. Hyland and C.-H. Luke Ong. On full abstraction for PCF: i, ii, and III. Inf. Comput., 163(2):285-408, 2000. URL: https://doi.org/10.1006/INCO.2000.2917.
  14. Guilhem Jaber. Operational nominal game semantics. In Andrew M. Pitts, editor, Foundations of Software Science and Computation Structures - 18th International Conference, FoSSaCS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings, Lecture Notes in Computer Science, pages 264-278. Springer, 2015. URL: https://doi.org/10.1007/978-3-662-46678-0_17.
  15. Guilhem Jaber and Andrzej S. Murawski. Complete trace models of state and control. In Nobuko Yoshida, editor, Programming Languages and Systems - 30th European Symposium on Programming, ESOP 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, volume 12648 of Lecture Notes in Computer Science, pages 348-374. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-72019-3_13.
  16. Guilhem Jaber and Andrzej S. Murawski. Compositional relational reasoning via operational game semantics. In 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021, pages 1-13. IEEE, 2021. URL: https://doi.org/10.1109/LICS52264.2021.9470524.
  17. Guilhem Jaber and Davide Sangiorgi. Games, mobile processes, and functions. In Florin Manea and Alex Simpson, editors, 30th EACSL Annual Conference on Computer Science Logic, CSL 2022, Göttingen, Germany (Virtual Conference), February 14-19, 2022, LIPIcs, pages 25:1-25:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.CSL.2022.25.
  18. Guilhem Jaber and Nicolas Tabareau. Kripke open bisimulation - A marriage of game semantics and operational techniques. In Xinyu Feng and Sungwoo Park, editors, Programming Languages and Systems - 13th Asian Symposium, APLAS 2015, Pohang, South Korea, November 30 - December 2, 2015, Proceedings, Lecture Notes in Computer Science, pages 271-291. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-26529-2_15.
  19. Alan Jeffrey and Julian Rathke. A theory of bisimulation for a fragment of concurrent ML with local names. Theor. Comput. Sci., 323(1-3):1-48, 2004. URL: https://doi.org/10.1016/J.TCS.2004.03.005.
  20. Alan Jeffrey and Julian Rathke. A fully abstract may testing semantics for concurrent objects. Theor. Comput. Sci., 338(1-3):17-63, 2005. URL: https://doi.org/10.1016/J.TCS.2004.10.012.
  21. Vasileios Koutavas and Mitchell Wand. Small bisimulations for reasoning about higher-order imperative programs. In J. Gregory Morrisett and Simon L. Peyton Jones, editors, Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2006, Charleston, South Carolina, USA, January 11-13, 2006, pages 141-152. ACM, 2006. URL: https://doi.org/10.1145/1111037.1111050.
  22. James Laird. Full abstraction for functional languages with control. In Proceedings, 12th Annual IEEE Symposium on Logic in Computer Science, Warsaw, Poland, June 29 - July 2, 1997, pages 58-67. IEEE Computer Society, 1997. URL: https://doi.org/10.1109/LICS.1997.614931.
  23. James Laird. A game semantics of idealized CSP. In Stephen D. Brookes and Michael W. Mislove, editors, Seventeenth Conference on the Mathematical Foundations of Programming Semantics, MFPS 2001, Aarhus, Denmark, May 23-26, 2001, Electronic Notes in Theoretical Computer Science, pages 232-257. Elsevier, 2001. URL: https://doi.org/10.1016/S1571-0661(04)80965-4.
  24. James Laird. A fully abstract trace semantics for general references. In Lars Arge, Christian Cachin, Tomasz Jurdzinski, and Andrzej Tarlecki, editors, Automata, Languages and Programming, 34th International Colloquium, ICALP 2007, Wroclaw, Poland, July 9-13, 2007, Proceedings, Lecture Notes in Computer Science, pages 667-679. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-73420-8_58.
  25. James Laird. A Curry-style semantics of interaction: From untyped to second-order lazy λμ-calculus. In Jean Goubault-Larrecq and Barbara König, editors, Foundations of Software Science and Computation Structures - 23rd International Conference, FOSSACS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, Lecture Notes in Computer Science, pages 422-441. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-45231-5_22.
  26. Søren B. Lassen and Paul Blain Levy. Typed normal form bisimulation for parametric polymorphism. In Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science, LICS 2008, 24-27 June 2008, Pittsburgh, PA, USA, pages 341-352. IEEE Computer Society, 2008. URL: https://doi.org/10.1109/LICS.2008.26.
  27. Sergueï Lenglet, Alan Schmitt, and Jean-Bernard Stefani. Characterizing contextual equivalence in calculi with passivation. Information and Computation, 209(11):1390-1433, 2011. URL: https://doi.org/10.1016/J.IC.2011.08.002.
  28. Ian Mason and Carolyn Talcott. Equivalence in functional languages with effects. Journal of Functional Programming, 1(3):287-327, 1991. URL: https://doi.org/10.1017/S0956796800000125.
  29. Andrzej S. Murawski and Nikos Tzevelekos. Game semantics for good general references. In Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science, LICS 2011, June 21-24, 2011, Toronto, Ontario, Canada, pages 75-84. IEEE Computer Society, 2011. URL: https://doi.org/10.1109/LICS.2011.31.
  30. Andrzej S. Murawski and Nikos Tzevelekos. Algorithmic games for full ground references. In Artur Czumaj, Kurt Mehlhorn, Andrew M. Pitts, and Roger Wattenhofer, editors, Automata, Languages, and Programming - 39th International Colloquium, ICALP 2012, Warwick, UK, July 9-13, 2012, Proceedings, Part II, volume 7392 of Lecture Notes in Computer Science, pages 312-324. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-31585-5_30.
  31. Amr Sabry and Matthias Felleisen. Reasoning about programs in continuation-passing style. In Jon L. White, editor, Proceedings of the Conference on Lisp and Functional Programming, LFP 1992, San Francisco, California, USA, 22-24 June 1992, pages 288-298. ACM, 1992. URL: https://doi.org/10.1145/141471.141563.
  32. Davide Sangiorgi. Expressing Mobility in Process Algebras: First-Order and Higher-Order Paradigms. PhD thesis CST-99-93, Department of Computer Science, University of Edinburgh, 1992. Google Scholar
  33. Davide Sangiorgi, Naoki Kobayashi, and Eijiro Sumii. Environmental bisimulations for higher-order languages. ACM Trans. Program. Lang. Syst., 33(1):5:1-5:69, 2011. URL: https://doi.org/10.1145/1889997.1890002.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact