# Niels Voorneveld: Behavioural equivalence via modalities for algebraic effects

Date: 12. 2. 2018

Source: Mathematics and theoretical computing seminar

Source: Mathematics and theoretical computing seminar

Č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.