Niels Voorneveld: Behavioural equivalence via modalities for algebraic effects
Source: Mathematics and theoretical computing seminar
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.