Accompanying material for the article 'no value restriction is needed for algebraic effects and handlers'

We present a straightforward, sound, Hindley-Milner polymorphic type system for algebraic effects and handlers in a call-by-value calculus, which, to our surprise, allows type variable generalisation of arbitrary computations, and not just values. The soundness of unrestricted call-by-value Hindley-Milner polymorphism is known to fail in the presence of computational effects such as reference cells and continuations, and many programming examples can be recast to use effect handlers instead of these effects. This file formalises in Twelf the calculus and its soundness proof.