{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T11:33:06Z","timestamp":1770291186927,"version":"3.49.0"},"reference-count":1,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2014,12,10]],"date-time":"2014-12-10T00:00:00Z","timestamp":1418169600000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>We present an effect system for core Eff, a simplified variant of Eff, which\nis an ML-style programming language with first-class algebraic effects and\nhandlers. We define an expressive effect system and prove safety of operational\nsemantics with respect to it. Then we give a domain-theoretic denotational\nsemantics of core Eff, using Pitts's theory of minimal invariant relations, and\nprove it adequate. We use this fact to develop tools for finding useful\ncontextual equivalences, including an induction principle. To demonstrate their\nusefulness, we use these tools to derive the usual equations for mutable state,\nincluding a general commutativity law for computations using non-interfering\nreferences. We have formalized the effect system, the operational semantics,\nand the safety theorem in Twelf.<\/jats:p>","DOI":"10.2168\/lmcs-10(4:9)2014","type":"journal-article","created":{"date-parts":[[2015,5,18]],"date-time":"2015-05-18T07:32:47Z","timestamp":1431934367000},"source":"Crossref","is-referenced-by-count":29,"title":["An Effect System for Algebraic Effects and Handlers"],"prefix":"10.46298","volume":"Volume 10, Issue 4","author":[{"given":"Andrej","family":"Bauer","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7755-2303","authenticated-orcid":false,"given":"Matija","family":"Pretnar","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2014,12,10]]},"reference":[{"key":"977:not-found"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/1153\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/1153\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T20:04:48Z","timestamp":1681243488000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/1153"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,12,10]]},"references-count":1,"URL":"https:\/\/doi.org\/10.2168\/lmcs-10(4:9)2014","relation":{"is-same-as":[{"id-type":"arxiv","id":"1306.6316","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1306.6316","asserted-by":"subject"}],"is-referenced-by":[{"id-type":"doi","id":"10.1145\/3009837.3009897","asserted-by":"subject"},{"id-type":"handle","id":"20.500.11820\/bd2598b0-20ce-4272-821f-985974bdd4f6","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"value":"1860-5974","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,12,10]]},"article-number":"1153"}}