Taro Sekiyama

When Types Intersect and Effects Get Handled

We introduce a novel intersection type system for a λ-calculus with algebraic effects and handlers. The system, inherently behavioral in nature, enjoys the classical properties of intersection type systems, in particular subject reduction and expansion. It thus characterizes the...