Coinductive Equivalences for Higher-order Coeffectful Languages

by Francesco Gavazzo


Coeffects and their associated type systems (such as graded modal types, quantitative types, and generalised bounded linear types) are becoming a standard programming language formalism to deal with context-dependent computations where code usage plays a central role. The theory of program equivalence for coeffectful languages, however, is considerably underdeveloped if compared to the denotational and operational semantics of such languages. This raises the question of how much of the theory of ordinary program equivalence can be given in a coeffectful scenario. In this talk, I will give an introduction to coinductive equivalences for higher-order programming languages with graded modal types modelling coeffectful behaviours. In particular, I will show how Abramsky’s applicative bisimilarity can be extended to deal with coeffectful behaviours. To maintain the talk as accessible as possible, I will not assume any previous knowledge on (coinductively-defined) notions of program equivalence, which I will gently introduce in the very first part of the seminar.

School of Computer and Cyber Sciences Augusta University