# LFCS Seminar: Danel Ahman

Normalization by evaluation and algebraic effects

We examine the interplay between computational effects and higher types by studying normalization by evaluation. We use algebraic theories to treat computational effects in a modular way. Our normalization algorithm and its correctness analysis are presented categorically by combining and extending various techniques from literature: we work in the category of covariant presheaves, we show how Filinski's residualizing extends to account for all algebraic effects, we ask the presheaves to come equipped with partial equivalence relations to account for equations on effect terms. Because many of the effect theories at hand are not strongly normalizing, we first show how to normalize the language modulo the equations on effect terms in a general case. However, sometimes we can do better and also normalize (part of) the effect theory by combining the free algebra monad of the effect theory and the residualizing monad in a suitable way. Our algorithm and its correctness proofs have also been formalized in Agda.

Joint work with Sam Staton from Cambridge.