Program Equivalence for Algebraic Effects via Modalities

TL;DR

This paper introduces a novel logic for algebraic effects in programming languages, establishing that logical equivalence, applicative bisimilarity, and contextual equivalence coincide, thus advancing understanding of program equivalence in effectful languages.

Contribution

It defines the first logic for algebraic effects where the induced equivalence matches contextual equivalence, unifying different notions of program equivalence.

Findings

Logical equivalence, applicative bisimilarity, and contextual equivalence coincide for the studied language.

The logic effectively characterizes properties of higher-order programs with algebraic effects.

This work provides a foundational tool for reasoning about program equivalence in effectful languages.

Abstract

This dissertation is concerned with the study of program equivalence and algebraic effects as they arise in the theory of programming languages. Algebraic effects represent impure behaviour in a functional programming language, such as input and output, exceptions, nondeterminism etc. all treated in a generic way. Program equivalence aims to identify which programs can be considered equal in some sense. This question has been studied for a long time but has only recently been extended to languages with algebraic effects, which are a newer development. Much work remains to be done in order to understand program equivalence in the presence of algebraic effects. In particular, there is no characterisation of contextual equivalence using a logic. We define a logic whose formulas express properties of higher-order programs with algebraic effects. We then investigate three notions of program equivalence for algebraic effects: logical equivalence induced by the aforementioned logic, applicative bisimilarity and contextual equivalence. For the programming language used in this dissertation, we prove that they all coincide. Therefore, the main novel contribution of the dissertation is defining the first logic for algebraic effects whose induced program equivalence coincides with contextual equivalence.