Niels Voorneveld, Tallinn University of Technology
Algebras for algebraic effects: Behavioural Equivalence of Effectful Programs
Algebraic effects describe interactions between a program and its environment, for instance to resolve some probabilistic choice, or to communicate with some global store. Algebraic effects in particular can be described using algebraic effect operations in the programming language. To give behavioural descriptions of effects we use algebras over a monad, which e.g. calculate expectations for probabilistic languages, or find the weakest precondition for programs interacting with a global store. If such algebras are sufficiently nice, they can be used to formulate a congruent notion of program equivalence.
We will look at different algebras for describing functional languages including algebraic effects such as nondeterminism, probability, global store, timer, and combinations thereof. We will moreover look at two methods for using these algebras to specify a notion of program equivalence: one by using them as quantitative modalities in a quantitative logic of behavioural properties, and one by constructing a relator used to define applicative bisimilarity. Lastly, we will briefly discuss more recent work: deriving algebras from equational theories, and combining effects and their algebras.