Niels Voorneveld: Behavioural equivalence via modalities for algebraic effects

Datum objave: 12. 2. 2018
Seminar za temelje matematike in teoretično računalništvo
Četrtek, 15. 2. 2018, od 11h do 13h, učilnica 3.07, Jadranska 21
Abstract: We investigate behavioural equivalence between programs in a call-by-value functional language extended with a signature of (algebraic) effect-triggering operations. Two programs are considered as being behaviourally equivalent if they enjoy the same behavioural properties. To formulate this, we define a logic whose formulas specify these behavioural properties. A crucial ingredient is a collection of modalities expressing effect-specific aspects of behaviour. We give a general theory of such modalities.

We look at two conditions, openness and decomposability, which if satisfied by the modalities makes the logically-specified behavioural equivalence compatible. Given upwards closed modalities, the behavioural equivalence is equal to a modality-defined notion of applicative bisimilarity, to which we can apply a generalisation of Howe's method. Throughout the talk we look at examples of effects satisfying the openness and decomposability property, which may include: error, non-determinism, probabilistic choice, global store and input/output.