We lay operational foundations for effect handlers. Introduced by
Plotkin and Pretnar, effect handlers are a novel programming construct
that generalises exception handlers, handling a range of computational
effects, such as I/O, state, and nondeterminism.

We describe a small-step structural operational semantics for a
higher-order calculus of effect handlers, along with a sound type
and effect system. We explore two alternative effect handler
implementation techniques: free monads, and delimited continuations.
Finally, time permitting, we show that Filinski’s monadic reflection
can be straightforwardly simulated by effect handlers.