Effect handlers are a powerful construct that can express complex programming abstractions. They are a generalisation of exception handlers that allow resumption from where the exception was raised. Crucially, allowing this resumption to happen at most once or in an unrestricted way has far-reaching consequences for a compiler that implements effect handlers. In addition to performance considerations, it breaks key rules of reasoning which has the effect of rendering many optimisations no longer sound. This research addresses this problem by giving a type system that can track the number of times a resumption happens even in the presence of nested resumptions and references that store them. As a result, a compiler can efficiently implement effect handlers by knowing how continuations will be used and which optimisations are sound for each expression. The type system is proven sound by modelling types and judgements semantically via a unary logical relation using the separation logic of Iris. By virtue of using Iris, we support recursive effect signatures and non-substructurally treated references which are needed to type non-trivial programs such as a library for cooperative concurrency.