Abstract Algebraic effects are computational effects that can be described with a set of basic operations and equations between them. As many interesting effect handlers do not respect these equations, most approaches assume a trivial theory, sacrificing both reasoning power and safety. We present an alternative approach where the type system tracks equations that are observed in subparts of the program, yielding a sound and flexible logic, and paving a way for practical optimisations and reasoning tools.

@article{LuksicP20,
  title = {Local algebraic effect theories},
  author = {ŽIGA LUKŠIČ and MATIJA PRETNAR},
  journal = {Journal of Functional Programming},
  volume = {30},
  year = {2020},
  doi = {10.1017/s0956796819000212}
}