Séminaire, 2 décembre 2021

Programme

10:30 – 12:00

Luca Reggio (Oxford University)

Invited talk: Game comonads: towards an axiomatic theory of resources

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.

14:00 – 15:00

Alexandra Silva (Cornell University)

Invited talk: Concurrent NetKAT: Modeling and analyzing stateful, concurrent networks

We introduce Concurrent NetKAT (CNetKAT), an extension of the network programming language NetKAT with multiple packets and with operators to specify and reason about concurrency and state in a network. We provide a model of the language based on partially ordered multisets, well-established mathematical structures in the denotational semantics of concurrent languages. We prove that CNetKAT is a sound and complete axiomatization of this model, and we illustrate the use of CNetKAT through various examples. More generally, CNetKAT is an algebraic framework to reason about programs with both local and global state. In our model these are, respectively, the packets and the global variable store, but the scope of applications is much more general, including reasoning about hardware pipelines inside an SDN switch.

This is joint work with Jana Wagemaker, Nate Foster, Tobias Kappe, Dexter Kozen, and Jurriaan Rot.

15:30 – 16:30

Francesco Gavazzo (Università di Bologna)

Invited talk: A Relational Theory of Effects and Coeffects

Graded modal types systems and coeffects are becoming a standard formalism to deal with context-dependent, usage-sensitive computations, especially when combined with computational effects. From a semantic perspective, effectful and coeffectful languages have been studied mostly by means of denotational semantics and almost nothing has been done from the point of view of relational reasoning. This is quite surprising since many cornerstone results — such as non-interference and metric preservation — on concrete coeffects are inherently relational. In this talk, I will present a general theory and calculus of program relations for higher-order languages with combined effects and coeffects. The calculus builds upon classic relational notions to deal with effectful and higher-order features, and upon the novel notion of a corelator (or comonadic lax extension) to handle coeffects, relationally. I will show how the aforementioned relational theory provides a unifying framework for defining and studying the metatheory of the main notions of program equivalence and refinement, such as contextual and logical equivalence and approximation, and applicative (bi)similarity. As a main result, I will present a general congruence theorem showing how simple relational properties ensure congruence properties of a large family of effectful and coffectful program equivalences.