{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T00:47:45Z","timestamp":1775868465097,"version":"3.50.1"},"publisher-location":"Cham","reference-count":39,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031908965","type":"print"},{"value":"9783031908972","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T00:00:00Z","timestamp":1746057600000},"content-version":"vor","delay-in-days":120,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>We define a two sorted equational theory of algebraic effects that models concurrent shared state with preemptive interleaving, recovering Brookes\u2019s seminal 1996 trace-based model precisely. The decomposition allows us to analyse Brookes\u2019s model algebraically in terms of separate but interacting components. The multiple sorts partition terms into layers. We use two sorts: a \u201chold\u201d sort for layers that disallow interleaving of environment memory accesses, analogous to holding a global lock on the memory; and a \u201ccede\u201d sort for the opposite. The algebraic signature comprises of independent interlocking components: two new operators that switch between these sorts, delimiting the atomic layers, thought of as acquiring and releasing the global lock; non-deterministic choice; and state-accessing operators. The axioms similarly divide cleanly: the delimiters behave as a closure pair; all operators are strict, and distribute over non-empty non-deterministic choice; and non-deterministic global state obeys Plotkin and Power\u2019s presentation of global state. Our representation theorem expresses the free algebras over a two-sorted family of variables as sets of traces with suitable closure conditions. When the held sort has no variables, we recover Brookes\u2019s trace semantics. We define several other single-and two-sorted theories to elucidate the connection to Brookes\u2019s model via translation embeddings and equivalences.<\/jats:p>","DOI":"10.1007\/978-3-031-90897-2_18","type":"book-chapter","created":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T08:19:38Z","timestamp":1746001178000},"page":"377-398","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Two-sorted algebraic decompositions of Brookes\u2019s shared-state denotational semantics"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6507-3791","authenticated-orcid":false,"given":"Yotam","family":"Dvir","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2071-0929","authenticated-orcid":false,"given":"Ohad","family":"Kammar","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4305-6998","authenticated-orcid":false,"given":"Ori","family":"Lahav","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8496-6096","authenticated-orcid":false,"given":"Gordon","family":"Plotkin","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,5,1]]},"reference":[{"key":"18_CR1","doi-asserted-by":"publisher","unstructured":"Abramsky, S., Jung, A.: Domain Theory. In: Handbook of Logic in Computer Science, Oxford University Press (04 1995), ISBN 9780198537625, https:\/\/doi.org\/10.1093\/oso\/9780198537625.003.0001","DOI":"10.1093\/oso\/9780198537625.003.0001"},{"key":"18_CR2","doi-asserted-by":"crossref","unstructured":"Ad\u00e1mek, J., Rosick\u00fd, J., Vitale, E.M.: Algebraic Theories: A Categorical Introduction to General Algebra. Cambridge Tracts in Mathematics, Cambridge University Press (2010)","DOI":"10.1017\/CBO9780511760754"},{"key":"18_CR3","doi-asserted-by":"publisher","unstructured":"Bauer, A., Pretnar, M.: Programming with algebraic effects and handlers. J. Log. Algebraic Methods Program. 84(1) (2015), https:\/\/doi.org\/10.1016\/J.JLAMP.2014.02.001","DOI":"10.1016\/J.JLAMP.2014.02.001"},{"key":"18_CR4","doi-asserted-by":"publisher","unstructured":"Benton, N., Hofmann, M., Nigam, V.: Effect-dependent transformations for concurrent programs. In: PPDP, ACM (2016), https:\/\/doi.org\/10.1145\/2967973.2968602","DOI":"10.1145\/2967973.2968602"},{"key":"18_CR5","doi-asserted-by":"publisher","unstructured":"Bloom, S.L.: Varieties of ordered algebras. Journal of Computer and System Sciences 13(2) (1976), ISSN 0022-0000, https:\/\/doi.org\/10.1016\/S0022-0000(76)80030-X","DOI":"10.1016\/S0022-0000(76)80030-X"},{"key":"18_CR6","doi-asserted-by":"publisher","unstructured":"Brookes, S.D.: Full abstraction for a shared-variable parallel language. Inf. Comput. 127(2) (1996), https:\/\/doi.org\/10.1006\/inco.1996.0056","DOI":"10.1006\/inco.1996.0056"},{"key":"18_CR7","doi-asserted-by":"publisher","unstructured":"Castellan, S., Clairambault, P., Winskel, G.: The parallel intensionally fully abstract games model of pcf. In: LICS (2015), https:\/\/doi.org\/10.1109\/LICS.2015.31","DOI":"10.1109\/LICS.2015.31"},{"key":"18_CR8","doi-asserted-by":"publisher","unstructured":"Dodds, M., Batty, M., Gotsman, A.: Compositional verification of compiler optimisations on relaxed memory. In: ESOP, ETAPS, LNCS, vol. 10801, Springer (2018), https:\/\/doi.org\/10.1007\/978-3-319-89884-1_36","DOI":"10.1007\/978-3-319-89884-1_36"},{"key":"18_CR9","doi-asserted-by":"publisher","unstructured":"Dolan, S., Eliopoulos, S., Hillerstr\u00f6m, D., Madhavapeddy, A., Sivaramakrishnan, K.C., White, L.: Concurrent system programming with effect handlers. In: TFP, LNCS, vol. 10788, Springer (2017), https:\/\/doi.org\/10.1007\/978-3-319-89719-6_6","DOI":"10.1007\/978-3-319-89719-6_6"},{"key":"18_CR10","unstructured":"Dolan, S., White, L., Sivaramakrishnan, K.C., Yallop, J., Madhavapeddy, A.: Effective concurrency with algebraic effects (2015), OCaml Workshop"},{"key":"18_CR11","doi-asserted-by":"publisher","unstructured":"Dvir, Y., Kammar, O., Lahav, O.: An algebraic theory for shared-state concurrency. In: APLAS, LNCS, vol. 13658, Springer (2022), https:\/\/doi.org\/10.1007\/978-3-031-21037-2_1","DOI":"10.1007\/978-3-031-21037-2_1"},{"key":"18_CR12","doi-asserted-by":"publisher","unstructured":"Dvir, Y., Kammar, O., Lahav, O.: A denotational approach to release\/acquire concurrency. In: ESOP, ETAPS, LNCS, vol. 14577, Springer (2024), https:\/\/doi.org\/10.1007\/978-3-031-57267-8_5","DOI":"10.1007\/978-3-031-57267-8_5"},{"key":"18_CR13","doi-asserted-by":"publisher","unstructured":"Dvir, Y., Kammar, O., Lahav, O.: A brookes-style denotational semantics for release\/acquire concurrency. TOPLAS (Jan 2025), ISSN 0164-0925, https:\/\/doi.org\/10.1145\/3715096, just Accepted","DOI":"10.1145\/3715096"},{"key":"18_CR14","unstructured":"Dvir, Y., Kammar, O., Lahav, O., Plotkin, G.: Two-sorted algebraic decompositions of brookes\u2019s shared-state denotational semantics (2025), URL https:\/\/arxiv.org\/abs\/2501.15104"},{"key":"18_CR15","unstructured":"Hennessy, M.C.B., Plotkin, G.D.: Full abstraction for a simple parallel programming language. In: Mathematical Foundations of Computer Science, Springer, Berlin, Heidelberg (1979), ISBN 978-3-540-35088-0"},{"key":"18_CR16","doi-asserted-by":"crossref","unstructured":"Hoare, T.: Laws of programming: The algebraic unification of theories of concurrency. In: CONCUR 2014 \u2013 Concurrency Theory, Springer, Berlin, Heidelberg (2014), ISBN 978-3-662-44584-6","DOI":"10.1007\/978-3-662-44584-6_1"},{"key":"18_CR17","doi-asserted-by":"publisher","unstructured":"Hyland, M., Plotkin, G.D., Power, J.: Combining effects: Sum and tensor. Theor. Comput. Sci. 357(1-3) (2006), https:\/\/doi.org\/10.1016\/j.tcs.2006.03.013","DOI":"10.1016\/j.tcs.2006.03.013"},{"key":"18_CR18","doi-asserted-by":"publisher","unstructured":"Hyland, M., Power, J.: Discrete Lawvere theories and computational effects. Theoretical Computer Science 366(1) (2006), ISSN 0304-3975, https:\/\/doi.org\/10.1016\/j.tcs.2006.07.007, algebra and Coalgebra in Computer Science","DOI":"10.1016\/j.tcs.2006.07.007"},{"key":"18_CR19","doi-asserted-by":"publisher","unstructured":"Jeffrey, A., Riely, J.: On Thin Air Reads: Towards an Event Structures Model of Relaxed Memory. LMCS Volume 15, Issue 1 (Mar 2019), https:\/\/doi.org\/10.23638\/LMCS-15(1:33)2019","DOI":"10.23638\/LMCS-15(1:33)2019"},{"key":"18_CR20","doi-asserted-by":"publisher","unstructured":"Kammar, O., Levy, P.B., Moss, S.K., Staton, S.: A monad for full ground reference cells. In: LICS (2017), https:\/\/doi.org\/10.1109\/LICS.2017.8005109","DOI":"10.1109\/LICS.2017.8005109"},{"key":"18_CR21","doi-asserted-by":"publisher","unstructured":"Kavanagh, R., Brookes, S.: A denotational semantics for SPARC TSO. In: MFPS, ENTCS, vol. 341, Elsevier (2018), https:\/\/doi.org\/10.1016\/j.entcs.2018.03.025","DOI":"10.1016\/j.entcs.2018.03.025"},{"key":"18_CR22","doi-asserted-by":"publisher","unstructured":"Kozen, D.: Semantics of probabilistic programs. Journal of Computer and System Sciences 22(3) (1981), ISSN 0022-0000, https:\/\/doi.org\/10.1016\/0022-0000(81)90036-2","DOI":"10.1016\/0022-0000(81)90036-2"},{"key":"18_CR23","doi-asserted-by":"crossref","unstructured":"Lawvere, F.W.: Functorial Semantics of Algebraic Theories and Some Algebraic Problems in the context of Functorial Semantics of Algebraic Theories. Ph.D. thesis, Department of Mathematics (1963)","DOI":"10.1073\/pnas.50.5.869"},{"key":"18_CR24","unstructured":"Levy, P.B.: Possible world semantics for general storage in call-by-value. In: Computer Science Logic, Springer, Berlin, Heidelberg (2002), ISBN 978-3-540-45793-0"},{"key":"18_CR25","doi-asserted-by":"publisher","unstructured":"Melli\u00e8s, P.: Local states in string diagrams. In: RTA-TLCA, LNCS, vol. 8560, Springer (2014), https:\/\/doi.org\/10.1007\/978-3-319-08918-8_23","DOI":"10.1007\/978-3-319-08918-8_23"},{"key":"18_CR26","doi-asserted-by":"publisher","unstructured":"Moggi, E.: Notions of computation and monads. Inf. Comput. 93(1) (1991), https:\/\/doi.org\/10.1016\/0890-5401(91)90052-4","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"18_CR27","doi-asserted-by":"publisher","unstructured":"Paquet, H., Saville, P.: Effectful semantics in bicategories: strong, commutative, and concurrent pseudomonads. LICS, Association for Computing Machinery, New York, NY, USA (2024), ISBN 9798400706608, https:\/\/doi.org\/10.1145\/3661814.3662130","DOI":"10.1145\/3661814.3662130"},{"key":"18_CR28","unstructured":"Plotkin, G.D.: A powerdomain for countable non-determinism. In: Automata, Languages and Programming, Springer, Berlin, Heidelberg (1982), ISBN 978-3-540-39308-5"},{"key":"18_CR29","doi-asserted-by":"publisher","unstructured":"Plotkin, G.D.: Some Varieties of Equational Logic. Springer, Berlin, Heidelberg (2006), ISBN 978-3-540-35464-2, https:\/\/doi.org\/10.1007\/11780274_8","DOI":"10.1007\/11780274_8"},{"key":"18_CR30","doi-asserted-by":"publisher","unstructured":"Plotkin, G.D., Power, J.: Notions of computation determine monads. In: FOSSACS, ETAPS, LNCS, vol. 2303, Springer (2002), https:\/\/doi.org\/10.1007\/3-540-45931-6_24","DOI":"10.1007\/3-540-45931-6_24"},{"key":"18_CR31","doi-asserted-by":"publisher","unstructured":"Plotkin, G.D., Power, J.: Algebraic operations and generic effects. Applied Categorical Structures 11(3) (2003), ISSN 1572-9095, https:\/\/doi.org\/10.1023\/A:1023064908962","DOI":"10.1023\/A:1023064908962"},{"key":"18_CR32","doi-asserted-by":"publisher","unstructured":"Plotkin, G.D., Pretnar, M.: Handlers of algebraic effects. In: ESOP, ETAPS, LNCS, vol. 5502, Springer (2009), https:\/\/doi.org\/10.1007\/978-3-642-00590-9_7","DOI":"10.1007\/978-3-642-00590-9_7"},{"key":"18_CR33","doi-asserted-by":"publisher","unstructured":"Plotkin, G.D., Pretnar, M.: Handling algebraic effects. Log. Methods Comput. Sci. 9(4) (2013), https:\/\/doi.org\/10.2168\/LMCS-9(4:23)2013","DOI":"10.2168\/LMCS-9(4:23)2013"},{"key":"18_CR34","unstructured":"Rivas, E., Jaskelioff, M.: Monads with merging (Jun 2019), URL https:\/\/inria.hal.science\/hal-02150199, working paper or preprint"},{"key":"18_CR35","doi-asserted-by":"publisher","unstructured":"Sivaramakrishnan, K.C., Dolan, S., White, L., Kelly, T., Jaffer, S., Madhavapeddy, A.: Retrofitting effect handlers onto ocaml. In: PLDI, ACM (2021), https:\/\/doi.org\/10.1145\/3453483.3454039","DOI":"10.1145\/3453483.3454039"},{"key":"18_CR36","unstructured":"Sterling, J., Gratzer, D., Birkedal, L.: Denotational semantics of general store and polymorphism (2023), URL https:\/\/arxiv.org\/abs\/2210.02169"},{"key":"18_CR37","unstructured":"Tarlecki, A.: Some nuances of many-sorted universal algebra: A review. Bull. EATCS 104 (2011), URL http:\/\/eatcs.org\/beatcs\/index.php\/beatcs\/article\/view\/121"},{"key":"18_CR38","doi-asserted-by":"publisher","unstructured":"Turon, A.J., Wand, M.: A separation logic for refining concurrent objects. In: POPL, ACM (2011), https:\/\/doi.org\/10.1145\/1926385.1926415","DOI":"10.1145\/1926385.1926415"},{"key":"18_CR39","doi-asserted-by":"publisher","unstructured":"Xu, Q., de Roever, W.P., He, J.: The rely-guarantee method for verifying shared variable concurrent programs. Formal Aspects Comput. 9(2) (1997), https:\/\/doi.org\/10.1007\/BF01211617","DOI":"10.1007\/BF01211617"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-90897-2_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T08:19:41Z","timestamp":1746001181000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-90897-2_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031908965","9783031908972"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-90897-2_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"1 May 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FoSSaCS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Foundations of Software Science and Computation Structures","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hamilton, ON","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 May 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 May 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fossacs2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2025\/conferences\/fossacs\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}