# Behavioural Equivalence via Modalities for Algebraic Effects

arXiv: https://arxiv.org/abs/1904.08843 · HTML: https://mlsanity.com/paper/1904.08843/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 18 Apr 2019.

## Built on by (most cited first, 1 of 1)

- [Query and Conquer: Execution-Guided SQL Generation](https://mlsanity.com/paper/2503.24364/) (2025)

## Abstract (arXiv)

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.