Justified Sequences in String Diagrams: a Comparison Between Two Approaches to Concurrent Game Semantics

Authors Clovis Eberhart, Tom Hirschowitz

Thumbnail PDF


  • Filesize: 0.57 MB
  • 16 pages

Document Identifiers

Author Details

Clovis Eberhart
Tom Hirschowitz

Cite AsGet BibTex

Clovis Eberhart and Tom Hirschowitz. Justified Sequences in String Diagrams: a Comparison Between Two Approaches to Concurrent Game Semantics. In 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 72, pp. 10:1-10:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)


Recent developments of game semantics have given rise to new models of concurrent languages. On the one hand, an approach based on string diagrams has given models of CCS and the pi-calculus, and on the other hand, Tsukada and Ong have designed a games model for a non-deterministic lambda-calculus. There is an obvious, shallow relationship between the two approaches, as they both define innocent strategies as sheaves for a Grothendieck topology embedding "views" into "plays". However, the notions of views and plays differ greatly between the approaches: Tsukada and Ong use notions from standard game semantics, while the authors of this paper use string diagrams. We here aim to bridge this gap by showing that even though the notions of plays, views, and innocent strategies differ, it is mostly a matter of presentation.
  • Concurrency
  • Sheaves
  • Presheaf models
  • Game Semantics


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Samson Abramsky, Radha Jagadeesan, and Pasquale Malacaria. Full abstraction for PCF. Information and Computation, 163(2):409-470, 2000. URL: http://dx.doi.org/10.1006/inco.2000.2930.
  2. Samson Abramsky and Paul-André Melliès. Concurrent games and full completeness. In LICS, pages 431-442. IEEE, 1999. URL: http://dx.doi.org/10.1109/LICS.1999.782638.
  3. Pierre Boudes. Thick subtrees, games and experiments. In TLCA, volume 5608 of Lecture Notes in Computer Science, pages 65-79. Springer, 2009. URL: http://dx.doi.org/10.1007/978-3-642-02273-9_7.
  4. Clovis Eberhart and Tom Hirschowitz. Justified sequences in string diagrams: a comparison between two approaches to concurrent game semantics. Preprint, 2016. URL: https://hal.archives-ouvertes.fr/hal-01372582.
  5. Clovis Eberhart and Tom Hirschowitz. Game semantics as a singular functor, and definability as geometric realisation. working paper or preprint, 2017. URL: https://hal.archives-ouvertes.fr/hal-01527171.
  6. Clovis Eberhart, Tom Hirschowitz, and Thomas Seiller. An intensionally fully-abstract sheaf model for pi. In CALCO, volume 35 of LIPIcs, pages 86-100. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015. URL: http://dx.doi.org/10.4230/LIPIcs.CALCO.2015.86.
  7. Dan R. Ghica and Andrzej S. Murawski. Angelic semantics of fine-grained concurrency. In FoSSaCS, volume 2987 of Lecture Notes in Computer Science, pages 211-225. Springer, 2004. URL: http://dx.doi.org/10.1007/978-3-540-24727-2_16.
  8. René Guitart. Relations et carrés exacts. Annales des Sciences Mathématiques du Québec, 4(2):103-125, 1980. Google Scholar
  9. Tom Hirschowitz. Full abstraction for fair testing in CCS. In CALCO, volume 8089 of Lecture Notes in Computer Science, pages 175-190. Springer, 2013. URL: http://dx.doi.org/10.1007/978-3-642-40206-7_14.
  10. Tom Hirschowitz. Full abstraction for fair testing in CCS (expanded version). Logical Methods in Computer Science, 10(4), 2014. URL: http://dx.doi.org/10.2168/LMCS-10(4:2)2014.
  11. J. M. E. Hyland and C.-H. Luke Ong. On full abstraction for PCF: I, II, and III. Information and Computation, 163(2):285-408, 2000. URL: http://dx.doi.org/10.1006/inco.2000.2917.
  12. André Joyal, Mogens Nielsen, and Glynn Winskel. Bisimulation and open maps. In LICS, pages 418-427. IEEE, 1993. URL: http://dx.doi.org/10.1109/LICS.1993.287566.
  13. James Laird. Game semantics for higher-order concurrency. In FSTTCS, volume 4337 of Lecture Notes in Computer Science, pages 417-428. Springer, 2006. URL: http://dx.doi.org/10.1007/11944836_38.
  14. Paul-André Melliès. Asynchronous games 2: the true concurrency of innocence. In Proc. 15th International Conference on Concurrency Theory, volume 3170 of Lecture Notes in Computer Science, pages 448-465. Springer, 2004. URL: http://dx.doi.org/10.1007/978-3-540-28644-8_29.
  15. Paul-André Melliès. Game semantics in string diagrams. In LICS, pages 481-490. IEEE, 2012. URL: http://dx.doi.org/10.1109/LICS.2012.58.
  16. Hanno Nickau. Hereditarily sequential functionals. In LFCS, volume 813 of Lecture Notes in Computer Science, pages 253-264. Springer, 1994. URL: http://dx.doi.org/10.1007/3-540-58140-5_25.
  17. M. Nielsen, G. Plotkin, and G. Winskel. Event structures and domains, part 1. Theoretical Computer Science, 13:65-108, 1981. Google Scholar
  18. Silvain Rideau and Glynn Winskel. Concurrent strategies. In LICS, pages 409-418. IEEE, 2011. URL: http://dx.doi.org/10.1109/LICS.2011.13.
  19. Takeshi Tsukada and C.-H. Luke Ong. Nondeterminism in game semantics via sheaves. In LICS. IEEE, 2015. Google Scholar
  20. Takeshi Tsukada and C.-H. Luke Ong. Plays as resource terms via non-idempotent intersection types. In LICS, pages 237-246. ACM, 2016. URL: http://dx.doi.org/10.1145/2933575.2934553.
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail