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