Game comonads, introduced by Abramsky, Dawar et al. in 2017, provide a categorical approach to finite model theory. A basic instance of this fremework allows to recover, in a purely syntax-free way, the following ingredients: the Ehrenfeucht-Fraïssé game, fragments of first-order logic with bounded quantifier rank (and variations thereof), and the combinatorial parameter of tree-depth. Other instances cover, e.g., k-pebble games and bisimulation games, and the corresponding logic fragments and combinatorial parameters.

After an introduction to game comonads, I shall present an axiomatic framework which captures the essential common features of these constructions. This is based on the notion of arboreal cover, a resource-indexed family of adjunctions with some `process category' - which unfolds relational structures into treelike forms, allowing resource parameters to be assigned to these unfoldings. Beyond this basic level, a landscape is beginning to emerge, in which structural features of the resource categories and comonads are reflected in degrees of tractability of the corresponding logic fragments.

I will then discuss an application of game comonads to homomorphism counting results in finite model theory. The prototypical homomorphism counting result is Lovasz' theorem (1967), stating that graphs A and B are isomorphic if and only if, for every graph C, the number of homomorphisms from C to A is the same as the number of homomorphisms from C to B. Game comonads yield uniform proofs of Lovasz' theorem and more recent results of Dvorak (2010) and Grohe (2020), as well as a novel homomorphism counting result in modal logic.