{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T23:05:56Z","timestamp":1779836756361,"version":"3.53.1"},"reference-count":28,"publisher":"Cambridge University Press (CUP)","license":[{"start":{"date-parts":[[2020,5,11]],"date-time":"2020-05-11T00:00:00Z","timestamp":1589155200000},"content-version":"unspecified","delay-in-days":131,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2020]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>Algebraic effects are computational effects that can be described with a set of basic operations and equations between them. As many interesting effect handlers do not respect these equations, most approaches assume a trivial theory, sacrificing both reasoning power and safety. We present an alternative approach where the type system tracks equations that are observed in subparts of the program, yielding a sound and flexible logic, and paving a way for practical optimisations and reasoning tools.<\/jats:p>","DOI":"10.1017\/s0956796819000212","type":"journal-article","created":{"date-parts":[[2020,5,11]],"date-time":"2020-05-11T05:26:11Z","timestamp":1589174771000},"source":"Crossref","is-referenced-by-count":7,"title":["Local algebraic effect theories"],"prefix":"10.1017","volume":"30","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9701-9418","authenticated-orcid":false,"given":"\u017dIGA","family":"LUK\u0160I\u010c","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"MATIJA","family":"PRETNAR","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2020,5,11]]},"reference":[{"key":"S0956796819000212_ref26","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2015.12.003"},{"key":"S0956796819000212_ref24","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-9(4:23)2013"},{"key":"S0956796819000212_ref23","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_7"},{"key":"S0956796819000212_ref10","doi-asserted-by":"crossref","unstructured":"de Moura, L. M. & Bj\u00f8rner, N. (2008) Z3: An efficient SMT solver. In TACAS. Lecture Notes in Computer Science, vol. 4963. Springer, pp. 337\u2013340.","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"S0956796819000212_ref8","first-page":"104","article-title":"Algebraic effect handlers go mainstream","volume":"8","author":"Chandrasekaran","year":"2018","journal-title":"Dagstuhl Rep."},{"key":"S0956796819000212_ref6","article-title":"Handle with care: Relational interpretation of algebraic effects and handlers","volume":"2","author":"Biernacki","year":"2018","journal-title":"PACMPL"},{"key":"S0956796819000212_ref17","doi-asserted-by":"crossref","unstructured":"Leijen, D. (2017) Type directed compilation of row-typed algebraic effects. In Castagna, G. & Gordon, A. D. (eds), Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18\u201320, 2017. ACM, pp. 486\u2013499.","DOI":"10.1145\/3009837.3009872"},{"key":"S0956796819000212_ref21","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45315-6_1"},{"key":"S0956796819000212_ref1","unstructured":"Ahman, D. (2017) Fibred Computational Effects. Ph.D. thesis, School of Informatics, University of Edinburgh."},{"key":"S0956796819000212_ref9","doi-asserted-by":"crossref","unstructured":"Claessen, K. & Hughes, J. (2000) Quickcheck: A lightweight tool for random testing of haskell programs. In Odersky, M. & Wadler, P. (eds), Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP\u201900), Montreal, Canada, September 18\u201321, 2000. ACM, pp. 268\u2013279.","DOI":"10.1145\/351240.351266"},{"key":"S0956796819000212_ref7","doi-asserted-by":"crossref","unstructured":"Brady, E. (2013) Programming and reasoning with algebraic effects and dependent types. In Morrisett, G. & Uustalu, T. (eds), ACM SIGPLAN International Conference on Functional Programming, ICFP\u201913, Boston, MA, USA, September 25\u201327, 2013. ACM, pp. 133\u2013144.","DOI":"10.1145\/2500365.2500581"},{"key":"S0956796819000212_ref16","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500590"},{"key":"S0956796819000212_ref3","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-10(4:9)2014"},{"key":"S0956796819000212_ref28","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2008.45"},{"key":"S0956796819000212_ref20","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1016\/0890-5401(91)90052-4","article-title":"Notions of computation and monads","volume":"93","author":"Moggi","year":"1991","journal-title":"Inf. Comput."},{"key":"S0956796819000212_ref4","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2014.02.001"},{"key":"S0956796819000212_ref19","unstructured":"McLaughlin, C. , McKinna, J. & Stark, I. (2018) Triangulating context lemmas. In Andronick, J. & Felty, A. P. (eds), Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018, Los Angeles, CA, USA, January 8\u20139, 2018. ACM, pp. 102\u2013114."},{"key":"S0956796819000212_ref27","doi-asserted-by":"crossref","unstructured":"Saleh, A. H. , Karachalias, G. , Pretnar, M. & Schrijvers, T. (2018) Explicit effect subtyping. In Ahmed, A. (ed), Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14\u201320, 2018, Proceedings. Lecture Notes in Computer Science, vol. 10801. Springer, pp. 327\u2013354.","DOI":"10.1007\/978-3-319-89884-1_12"},{"key":"S0956796819000212_ref25","unstructured":"Pretnar, M. (2010) Logic and Handling of Algebraic Effects. Ph.D. thesis, University of Edinburgh, UK."},{"key":"S0956796819000212_ref22","doi-asserted-by":"publisher","DOI":"10.1023\/A:1023064908962"},{"key":"S0956796819000212_ref11","first-page":"1","article-title":"On the expressive power of user-defined effects: Effect handlers, monadic reflection, delimited control","volume":"1","author":"Forster","year":"2017","journal-title":"PACMPL"},{"key":"S0956796819000212_ref12","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034777"},{"key":"S0956796819000212_ref5","first-page":"44","article-title":"From theory to practice of algebraic effects and handlers","volume":"6","author":"Bauer","year":"2016","journal-title":"Dagstuhl Rep."},{"key":"S0956796819000212_ref13","doi-asserted-by":"publisher","DOI":"10.1145\/2976022.2976033"},{"key":"S0956796819000212_ref14","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103698"},{"key":"S0956796819000212_ref2","first-page":"1","article-title":"Handling fibred algebraic effects","volume":"2","author":"Ahman","year":"2018","journal-title":"PACMPL"},{"key":"S0956796819000212_ref15","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796816000320"},{"key":"S0956796819000212_ref18","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00088-9"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796819000212","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T22:36:51Z","timestamp":1779835011000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796819000212\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"references-count":28,"alternative-id":["S0956796819000212"],"URL":"https:\/\/doi.org\/10.1017\/s0956796819000212","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"article-number":"e13"}}