
doi: 10.1145/3290336
Game semantics is the art of interpreting types as games and programs as strategies interacting in space and time with their environment. In order to reflect the interactive behavior of programs, strategies are required to follow specific scheduling policies. Typically, in the case of a purely sequential programming language, the program (Player) and its environment (Opponent) will play one after the other, in a strictly alternating way. On the other hand, in the case of a concurrent language, Player and Opponent will be allowed to play several moves in a row, in a non-alternating way. In both cases, the scheduling policy is designed very carefully in order to ensure that the strategies synchronize properly and compose well when plugged together. A longstanding conceptual problem has been to understand when and why a given scheduling policy works and is compositional in that sense. In this paper, we exhibit a number of simple and fundamental combinatorial structures which ensure that a given scheduling policy encoded as synchronization template defines a symmetric monoidal closed (and in fact star-autonomous) bicategory of games, strategies and simulations. To that purpose, we choose to work at a very general level, and illustrate our method by constructing two template game models of linear logic with different flavors (alternating and non-alternating) using the same categorical combinatorics, performed in the category of small categories. As a whole, the paper may be seen as a hymn in praise of synchronization, building on the notion of synchronization algebra in process calculi and adapting it smoothly to programming language semantics, using a combination of ideas at the converging point of game semantics and of categorical algebra.
Synchronization algebras, Denotational semantics, [MATH.MATH-QA] Mathematics [math]/Quantum Algebra [math.QA], [INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO], Game semantics, [MATH.MATH-AG] Mathematics [math]/Algebraic Geometry [math.AG], [MATH.MATH-AT] Mathematics [math]/Algebraic Topology [math.AT], [MATH.MATH-CT] Mathematics [math]/Category Theory [math.CT], [INFO.INFO-PL] Computer Science [cs]/Programming Languages [cs.PL], Template games, [INFO.INFO-MS] Computer Science [cs]/Mathematical Software [cs.MS], [INFO.INFO-CL] Computer Science [cs]/Computation and Language [cs.CL], Concurrency, Categorical semantics, Concurrent non-alternating games, Bicategorical models of linear logic, [INFO.INFO-GT] Computer Science [cs]/Computer Science and Game Theory [cs.GT], [MATH.MATH-LO] Mathematics [math]/Logic [math.LO], Sequential alternating games, Theory of computation, [INFO.INFO-FL] Computer Science [cs]/Formal Languages and Automata Theory [cs.FL]
Synchronization algebras, Denotational semantics, [MATH.MATH-QA] Mathematics [math]/Quantum Algebra [math.QA], [INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO], Game semantics, [MATH.MATH-AG] Mathematics [math]/Algebraic Geometry [math.AG], [MATH.MATH-AT] Mathematics [math]/Algebraic Topology [math.AT], [MATH.MATH-CT] Mathematics [math]/Category Theory [math.CT], [INFO.INFO-PL] Computer Science [cs]/Programming Languages [cs.PL], Template games, [INFO.INFO-MS] Computer Science [cs]/Mathematical Software [cs.MS], [INFO.INFO-CL] Computer Science [cs]/Computation and Language [cs.CL], Concurrency, Categorical semantics, Concurrent non-alternating games, Bicategorical models of linear logic, [INFO.INFO-GT] Computer Science [cs]/Computer Science and Game Theory [cs.GT], [MATH.MATH-LO] Mathematics [math]/Logic [math.LO], Sequential alternating games, Theory of computation, [INFO.INFO-FL] Computer Science [cs]/Formal Languages and Automata Theory [cs.FL]
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 8 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Top 10% | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Top 10% |
