Categorical logical relations for effects and handlers

Effects and handlers are a powerful programming language control flow construct based on delimited continuations, and can express diverse effects such as nondeterminism, concurrency, and state management. Furthermore, they excel in abstracting and composing effects. Logical relations are proof method where a predicate or relation is assigned to each type in a way compatible with the language's constructs.

In my thesis, I extended Shin-ya Katsumata's category theoretic "fibrations for logical relations" to effects and handlers, and used them to prove correctness for some basic automatic differentiation algorithms.

I will give a short introduction to logical relations, the semantics of effects and handlers, and how I used fibrations for logical relations (FFLRs), with an emphasis on how FFLRs can be used to simply and incrementally build theories of logical relations.