Francesco Gavazzo (Università di Bologna), 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.