We present an effect system for core Eff, a simplified variant of Eff, whichis an ML-style programming language with first-class algebraic effects andhandlers. We define an expressive effect system and prove safety of operationalsemantics with respect to it. Then we give a domain-theoretic denotationalsemantics of core Eff, using Pitts's theory of minimal invariant relations, andprove it adequate. We use this fact to develop tools for finding usefulcontextual equivalences, including an induction principle. To demonstrate theirusefulness, we use these tools to derive the usual equations for mutable state,including a general commutativity law for computations using non-interferingreferences. We have formalized the effect system, the operational semantics,and the safety theorem in Twelf.
展开▼
