ABSTRACT. In this proposed talk, we will present work in progress towards a “primitive” categorical structure for concurrent game semantics: a categorical structure that is simple and lets us derive categorically familiar models of various languages and evaluation strategies.

ABSTRACT. Bidirectional information flow is a central concept in both categorical game semantics and practical functional programming. In game semantics, the Joyal-Street-Verity's Int construction provides a canonical way to build compact closed categories from traced monoidal categories, elegantly modeling bidirectional interaction and feedback loops. Conversely, in functional programming, the Lens construction offers a robust, compositional framework for bidirectional state access and update. This work-in-progress explores the structural relationship between these two paradigms. We propose an adjunction between the categories arising from the Lens and Int constructions. By formally connecting the state-based approach of the Lens construction with the traced monoidal approach of the Int construction, we aim to bridge abstract game-semantic models with compositional theories of bidirectional flow. In this talk, we will outline the core functorial mappings between these categories, present the ongoing proofs of the adjunction, and discuss its potential applications to the foundations of game semantics.

ABSTRACT. For a first-order language with full ground references and iteration, we give an explicit denotational semantics. A type denotes a “platform set”, which is a family of “platforms” that indicate the references included. A state is represented as a tree, showing the result of following chains of references, whose nodes are partitioned into finitely many equivalence classes, showing the aliasing. The model is equivalent to known models that use ends or coends, or strong nominal sets, but is simpler in the sense that a morphism is simply a function.

ABSTRACT. Operational game semantics are presented through labelled transition systems, of which the induced bisimilarity on programs is shown to be included in CIU equivalence, a variant of contextual equivalence. Soundness of operational game semantics follows from external context lemmas which state that CIU and contextual equivalences coincide. This talk will show how one may avoid the use of CIU equivalence entirely, by changing the initial operational configurations of terms in the operational game semantics. The construction is inspired by a proof technique for the genericity lemma due to Takahashi.

ABSTRACT. We study contextual interactions in an ML-like language equipped with general references and continuations through the lens of operational game semantics, focusing on the reachability and approximation problems. Previous work showed that these problems are decidable in the loop-free setting via automata over nested data, where bounded P-views admit a finite representation. With the addition of loops, however, P-views become unbounded, and these techniques no longer apply. We introduce a new class of automata over infinite alphabets that supports unbounded nesting of data, together with new restrictions of the P-view: the shallow P-view and enriched shallow P-view. These provide a finite representation of the relevant visible fragment of unbounded traces. We establish a precise correspondence between these automata and higher-order programs with loops: the trace semantics of any such program can be captured by an automaton, and conversely, the trace language of any such automaton can be realised by an imperative higher-order program with loops. This correspondence enables the transfer of decidability and undecidability results between the automata and programs. In particular, we show that adding loops preserves decidability of reachability, while rendering approximation undecidable.

ABSTRACT. We discuss how to solve whole hierarchies of behavioral equivalence problems as single quantitative problems about modal logics through energy games. My work on generalized equivalence checking of concurrent programs proposes the first unified way to check for whole ranges of equivalences. Its prototype implementation https://equiv.io can compute which notions from van Glabbeek's strong and weak linear-time–branching-time spectrum relate pairs of finite-state processes.