Séminaire, Dec. 2, 2021
La rencontre aura lieu en amphi B, à l'ENS de Lyon. Les exposés seront diffusés en ligne. Merci de vous inscrire si vous comptez être sur place à Lyon.
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 syntaxfree way, the following ingredients: the EhrenfeuchtFraïssé game, fragments of firstorder logic with bounded quantifier rank (and variations thereof), and the combinatorial parameter of treedepth. Other instances cover, e.g., kpebble 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 resourceindexed 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)
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, wellestablished 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 contextdependent, usagesensitive 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 noninterference and metric preservation — on concrete coeffects are inherently relational. In this talk, I will present a general theory and calculus of program relations for higherorder languages with combined effects and coeffects. The calculus builds upon classic relational notions to deal with effectful and higherorder 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.