# Behavioural Equivalence via Modalities for Algebraic Effects

## TL;DR

This paper develops a logic with effect-specific modalities to characterize behavioural equivalence in effectful functional programs, ensuring congruence under certain conditions for various algebraic effects.

## Contribution

It introduces a general theory of modalities for behavioural equivalence, establishing conditions for their effectiveness and applicability to multiple algebraic effects.

## Key findings

- Modalities satisfy openness and decomposability for several effects
- Behavioural equivalence coincides with applicative bisimilarity under these modalities
- The approach ensures congruence via a generalized Howe's method

## Abstract

The paper investigates 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 behavioural properties. A crucial ingredient is a collection of modalities expressing effect-specific aspects of behaviour. We give a general theory of such modalities. If two conditions, openness and decomposability, are satisfied by the modalities then the logically specified behavioural equivalence coincides with a modality-defined notion of applicative bisimilarity, which can be proven to be a congruence by a generalisation of Howe's method. We show that the openness and decomposability conditions hold for several examples of algebraic effects: nondeterminism, probabilistic choice, global store and input/output.