Programming and Reasoning with Algebraic Effects and Dependent Types (cs.st-andrews.ac.uk)