Coinductive Equivalences for Higher-order Coeffectful Languages
- When: Friday, 02/04/2021, between 1pm and 2pm EST (6pm - 7pm UTC)
- Where: Zoom; Outside guests please RSVP by emailing Harley Eades
- YouTube Stream/Recording: https://youtu.be/-tgA2zShDcQ
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.