Skip to content

wikku/normalization-effect-handlers

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

Normalization for algebraic effect handlers

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”

About

Normalization for Algebraic Effect Handlers

Resources

Stars

Watchers

Forks