A proof of normalization (termination of evaluation) for a language [PPS19] with polymorphic algebraic effects. It relies on direct-style unary logical relations defined as a fixed-point, inspired by the step-indexed biorthogonal binary relations in [Bie+18].
[Bie+18] Dariusz Biernacki et al. “Handle with care: relational interpretation of algebraic effects and handlers”.
[PPS19] Maciej Piróg, Piotr Polesiuk, and Filip Sieczkowski. “Typed Equivalence of Effect Handlers and Delimited Control”