{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T14:12:29Z","timestamp":1784211149792,"version":"3.55.0"},"reference-count":48,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T00:00:00Z","timestamp":1767830400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"funder":[{"name":"Royal Society University Research Fellowship","award":["Foundations for type-driven data science"],"award-info":[{"award-number":["Foundations for type-driven data science"]}]},{"name":"UKRI Future Leaders Fellowship","award":["MR\/T043830\/1 and MR\/Z000351\/1"],"award-info":[{"award-number":["MR\/T043830\/1 and MR\/Z000351\/1"]}]},{"name":"UK Advanced Research and Invention Agency","award":["Qbs4Safety: Core Representation Underlying Safeguarded AI"],"award-info":[{"award-number":["Qbs4Safety: Core Representation Underlying Safeguarded AI"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2026,1,8]]},"abstract":"<jats:p>We use the theory of algebraic effects to give a complete equational axiomatization for dynamic threads. Our method is based on parameterized algebraic theories, which give a concrete syntax for strong monads on functor categories, and are a convenient framework for names and binding.<\/jats:p>\n                  <jats:p>Our programs are built from the key primitives \u2018fork\u2019 and \u2018wait\u2019. \u2018Fork\u2019 creates a child thread and passes its name (thread ID) to the parent thread. \u2018Wait\u2019 allows us to wait for given child threads to finish. We provide a parameterized algebraic theory built from fork and wait, together with basic atomic actions and laws such as associativity of \u2018fork\u2019.<\/jats:p>\n                  <jats:p>Our equational axiomatization is complete in two senses. First, for closed expressions, it completely captures equality of labelled posets (pomsets), an established model of concurrency: model complete. Second, any two open expressions are provably equal if they are equal under all closing substitutions: syntactically complete.<\/jats:p>\n                  <jats:p>The benefit of algebraic effects is that the semantic analysis can focus on the algebraic operations of fork and wait. We then extend the analysis to a simple concurrent programming language by giving operational and denotational semantics. The denotational semantics is built using the methods of parameterized algebraic theories and we show that it is sound, adequate, and fully abstract at first order for labelled-poset observations.<\/jats:p>","DOI":"10.1145\/3776706","type":"journal-article","created":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T18:59:43Z","timestamp":1767898783000},"page":"1847-1875","update-policy":"https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["An Equational Axiomatization of Dynamic Threads via Algebraic Effects: Presheaves on Finite Relations, Labelled Posets, and Parameterized Algebraic Theories"],"prefix":"10.1145","volume":"10","author":[{"ORCID":"https:\/\/2.zoppoz.workers.dev:443\/https\/orcid.org\/0000-0002-2071-0929","authenticated-orcid":false,"given":"Ohad","family":"Kammar","sequence":"first","affiliation":[{"name":"University of Edinburgh, Edinburgh, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/2.zoppoz.workers.dev:443\/https\/orcid.org\/0009-0005-7121-8095","authenticated-orcid":false,"given":"Jack","family":"Liell-Cock","sequence":"additional","affiliation":[{"name":"University of Oxford, Oxford, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/2.zoppoz.workers.dev:443\/https\/orcid.org\/0000-0002-1360-4714","authenticated-orcid":false,"given":"Sam","family":"Lindley","sequence":"additional","affiliation":[{"name":"University of Edinburgh, Edinburgh, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/2.zoppoz.workers.dev:443\/https\/orcid.org\/0009-0003-6036-6426","authenticated-orcid":false,"given":"Cristina","family":"Matache","sequence":"additional","affiliation":[{"name":"University of Edinburgh, Edinburgh, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/2.zoppoz.workers.dev:443\/https\/orcid.org\/0000-0002-7149-3805","authenticated-orcid":false,"given":"Sam","family":"Staton","sequence":"additional","affiliation":[{"name":"University of Oxford, Oxford, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,1,8]]},"reference":[{"key":"e_1_3_2_2_2","unstructured":"2024. IEEE Standard for Information Technology\u2014Portable Operating System Interface (POSIX\u00ae) Base Specifications Issue 8. https:\/\/2.zoppoz.workers.dev:443\/https\/pubs.opengroup.org\/onlinepubs\/9799919799\/ Approved 2024. Published by IEEE and The Open Group."},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","unstructured":"Mart\u00edn Abadi and Gordon D. Plotkin. 2010. A Model of Cooperative Threads. Log. Methods Comput. Sci. 6 4 (2010). doi:10.2168\/LMCS-6(4:2)2010","DOI":"10.2168\/LMCS-6(4:2)2010"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","unstructured":"Rajeev Alur Caleb Stanford and Christopher Watson. 2023. A Robust Theory of Series Parallel Graphs. Proceedings of the ACM on Programming Languages 7 POPL (2023) Article 37. doi:10.1145\/3571230","DOI":"10.1145\/3571230"},{"key":"e_1_3_2_5_2","doi-asserted-by":"crossref","unstructured":"John C. Baez Brandon Coya and Franciscus Rebro. 2018. Props in Network Theory. Theory and Applications of Categories 33 (2018) 727\u2013783. https:\/\/2.zoppoz.workers.dev:443\/http\/www.tac.mta.ca\/tac\/volumes\/33\/25\/33-25.pdf","DOI":"10.70930\/tac\/mgee83ch"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","unstructured":"Nick Benton Martin Hofmann and Vivek Nigam. 2016. Effect-dependent transformations for concurrent programs. In PPDP. ACM. doi:10.1145\/2967973.2968602","DOI":"10.1145\/2967973.2968602"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","unstructured":"Jan A. Bergstra Alban Ponse and Scott A. Smolka (Eds.). 2001. Handbook of Process Algebra. Elsevier. doi:10.1016\/B978-0-444-82830-9.X5017-6","DOI":"10.1016\/B978-0-444-82830-9.X5017-6"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","unstructured":"Filippo Bonchi Pawe\u0142 Soboci\u0144ski and Fabio Zanasi. 2017. The Calculus of Signal Flow Diagrams I: Linear relations on streams. Inform. Comput. (2017) 2\u201329. doi:10.1016\/j.ic.2016.03.002","DOI":"10.1016\/j.ic.2016.03.002"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","unstructured":"Stephen D. Brookes. 1996. Full Abstraction for a Shared-Variable Parallel Language. Inform. Comput. 127 2 (1996). doi:10.1006\/inco.1996.0056","DOI":"10.1006\/inco.1996.0056"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","unstructured":"Paulo Em\u00edlio de Vilhena and Fran\u00e7ois Pottier. 2021. A separation logic for effect handlers. Proc. ACM Program. Lang. 5 POPL (2021) 1\u201328. doi:10.1145\/3434314","DOI":"10.1145\/3434314"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","unstructured":"Yotam Dvir Ohad Kammar and Ori Lahav. 2024. A Denotational Approach to Release\/Acquire Concurrency. In ESOP ETAPS (LNCS Vol. 14577). Springer. doi:10.1007\/978-3-031-57267-8_5","DOI":"10.1007\/978-3-031-57267-8_5"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","unstructured":"Yotam Dvir Ohad Kammar Ori Lahav and Gordon D. Plotkin. 2025. Two-sorted algebraic decompositions of Brookes's shared-state denotational semantics. (2025). doi:10.1007\/978-3-031-90897-2_18","DOI":"10.1007\/978-3-031-90897-2_18"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","unstructured":"Uli Fahrenberg Christian Johansen Georg Struth and Krzysztof Ziemia\u0144ski. 2022. Posets with interfaces as a model for concurrency. Inform. Comput. 285 (2022). doi:10.1016\/j.ic.2022.104914","DOI":"10.1016\/j.ic.2022.104914"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","unstructured":"Jay L. Gischer. 1988. The equational theory of pomsets. Theor. Comput. Sci. 61 (1988). doi:10.1016\/0304-3975(88)90124-7","DOI":"10.1016\/0304-3975(88)90124-7"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","unstructured":"Tony Hoare Bernhard M\u00f6ller Georg Struth and Ian Wehrman. 2011. Concurrent Kleene algebra and its foundations. J. Logic Alg. Program. 80 6 (2011). doi:10.1016\/j.jlap.2011.04.005","DOI":"10.1016\/j.jlap.2011.04.005"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","unstructured":"Tony Hoare and Stephan van Staden. 2014. The laws of programming unify process calculi. Sci. Comput. Program. 85 (2014) 102\u2013114. doi:10.1016\/j.scico.2013.08.012","DOI":"10.1016\/j.scico.2013.08.012"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","unstructured":"Martin Hyland Gordon D. Plotkin and John Power. 2006. Combining Effects: Sum and Tensor. Theor. Comput. Sci. 357 1 (July 2006) 70\u201399. doi:10.1016\/j.tcs.2006.03.013","DOI":"10.1016\/j.tcs.2006.03.013"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","unstructured":"Radha Jagadeesan Gustavo Petri and James Riely. 2012. Brookes Is Relaxed Almost!. In FOSSACS ETAPS (LNCS Vol. 7213) Lars Birkedal (Ed.). Springer 180\u2013194. doi:10.1007\/978-3-642-28729-9_12","DOI":"10.1007\/978-3-642-28729-9_12"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","unstructured":"Ralf Jung Robbert Krebbers Jacques-Henri Jourdan Ales Bizjak Lars Birkedal and Derek Dreyer. 2018. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. J. Funct. Program. 28 (2018) e20. doi:10.1017\/S0956796818000151","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","unstructured":"Ohad Kammar Sam Lindley and Nicolas Oury. 2013. Handlers in action. In ICFP'13. ACM 145\u2013158. doi:10.1145\/2500365.2500590","DOI":"10.1145\/2500365.2500590"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","unstructured":"G. A. Kavvos. 2025. Adequacy for Algebraic Effects Revisited. Proc. ACM Program. Lang. 9 OOPSLA1 (2025) 927\u2013955. doi:10.1145\/3720457","DOI":"10.1145\/3720457"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","unstructured":"D\u00e9nes K\u00f6nig. 1926. Sur les correspondances multivoques des ensembles. Fundamenta Mathematicae 8 (1926) 114\u2013134. doi:10.4064\/fm-8-1-114-134","DOI":"10.4064\/fm-8-1-114-134"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","unstructured":"Paul Blain Levy John Power and Hayo Thielecke. 2003. Modelling environments in call-by-value programming languages. Inform. Comput. 185 2 (2003) 182\u2013210. doi:10.1016\/S0890-5401(03)00088-9","DOI":"10.1016\/S0890-5401(03)00088-9"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","unstructured":"Martin Markl. 2008. Operads and PROPs. Handbook of Algebra Vol. 5. North-Holland 87\u2013140. doi:10.1016\/S1570-7954(07)05002-4","DOI":"10.1016\/S1570-7954(07)05002-4"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","unstructured":"T.A. McKee. 1983. Series-parallel graphs: A logical approach. Journal of Graph Theory 7 2 (1983) 229\u2013236. doi:10.1002\/jgt.3190070206","DOI":"10.1002\/jgt.3190070206"},{"key":"e_1_3_2_26_2","unstructured":"Robin Milner. 1989. Communication and concurrency. Prentice Hall. https:\/\/2.zoppoz.workers.dev:443\/https\/dl.acm.org\/doi\/book\/10.5555\/534666"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","unstructured":"Eugenio Moggi. 1991. Notions of computation and monads. Inform. Computation(1991). doi:10.1016\/0890-5401(91)900524","DOI":"10.1016\/0890-5401(91)900524"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","unstructured":"Madhavan Mukund and Mogens Nielsen. 1992. CCS locations and asynchronous transition systems. In Proc. FSTTCS. doi:10.1007\/3-540-56287-7_116","DOI":"10.1007\/3-540-56287-7_116"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","unstructured":"Mogens Nielsen Gordon D. Plotkin and Glynn Winskel. 1981. Petri Nets Event Structures and domains Part I. Theoret. Comput. Sci. 13 (1981). doi:10.1016\/0304-3975(81)90112-2","DOI":"10.1016\/0304-3975(81)90112-2"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","unstructured":"Frank J. Oles. 1983. Type algebras functor categories and block structure. In Algebraic methods in semantics. doi:10.7146\/dpb.v12i156.7430","DOI":"10.7146\/dpb.v12i156.7430"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","unstructured":"Luna Phipps-Costin Andreas Rossberg Arjun Guha Daan Leijen Daniel Hillerstr\u00f6m K. C. Sivaramakrishnan Matija Pretnar and Sam Lindley. 2023. Continuing WebAssembly with Effect Handlers. Proc. ACM Program. Lang. 7 OOPSLA2 (2023) 460\u2013485. doi:10.1145\/3622814","DOI":"10.1145\/3622814"},{"key":"e_1_3_2_32_2","doi-asserted-by":"crossref","unstructured":"Andrew M Pitts. 2013. Nominal Sets: Names and Symmetry in Computer Science. CUP. https:\/\/2.zoppoz.workers.dev:443\/https\/dl.acm.org\/doi\/10.5555\/2512979","DOI":"10.1017\/CBO9781139084673"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","unstructured":"Gordon Plotkin. 2012. Concurrency and the Algebraic Theory of Effects. In Proc. CONCUR 2012. doi:10.1007\/978-3-642-32940-1_2","DOI":"10.1007\/978-3-642-32940-1_2"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","unstructured":"Gordon Plotkin and John Power. 2003. Algebraic operations and generic effects. Appl. Categ. Structures 11 1 (2003) 69\u201394. doi:10.1023\/A:1023064908962","DOI":"10.1023\/A:1023064908962"},{"key":"e_1_3_2_35_2","doi-asserted-by":"crossref","unstructured":"Gordon Plotkin and Vaughan Pratt. 1996. Teams can see pomsets. In OMIV \u201996: Proceedings of the DIMACS workshop on Partial order methods in verification. https:\/\/2.zoppoz.workers.dev:443\/https\/homepages.inf.ed.ac.uk\/gdp\/publications\/Teams.pdf","DOI":"10.1090\/dimacs\/029\/07"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","unstructured":"Gordon D. Plotkin and John Power. 2001. Adequacy for Algebraic Effects. In FOSSACS 2001. doi:10.1007\/3-540-45315-6_1","DOI":"10.1007\/3-540-45315-6_1"},{"key":"e_1_3_2_37_2","doi-asserted-by":"crossref","unstructured":"Gordon D. Plotkin and John Power. 2002. Notions of Computation Determine Monads. In FOSSACS 2002. Springer 342\u2013356. https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1007\/3-540-45931-6_24","DOI":"10.1007\/3-540-45931-6_24"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","unstructured":"Gordon D. Plotkin and Matija Pretnar. 2013. Handling Algebraic Effects. Log. Methods Comput. Sci. 9 4 (2013). doi:10.2168\/LMCS-9(4:23)2013","DOI":"10.2168\/LMCS-9(4:23)2013"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","unstructured":"Vaughan R. Pratt. 1986. Modeling concurrency with partial orders. Int. J. Parallel Program. 15 1 (1986) 33\u201371. doi:10.1007\/BF01379149","DOI":"10.1007\/BF01379149"},{"key":"e_1_3_2_40_2","doi-asserted-by":"crossref","unstructured":"Davide Sangiorgi and David Walker. 2001. The Pi-Calculus: A Theory of Mobile Processes. Cambridge University Press. https:\/\/2.zoppoz.workers.dev:443\/https\/dl.acm.org\/doi\/10.5555\/559050","DOI":"10.1017\/9781316134924"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","unstructured":"K. C. Sivaramakrishnan Stephen Dolan Leo White Tom Kelly Sadiq Jaffer and Anil Madhavapeddy. 2021. Retrofitting effect handlers onto OCaml. In PLDI \u201921. ACM 206\u2013221. doi:10.1145\/3453483.3454039","DOI":"10.1145\/3453483.3454039"},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","unstructured":"Ian Stark. 2008. Free-algebra models for the pi-calculus. Theor. Comput. Sci. 390 2-3 (2008) 248\u2013270. doi:10.1016\/J.TCS.2007.09.024","DOI":"10.1016\/J.TCS.2007.09.024"},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","unstructured":"Sam Staton. 2013. An Algebraic Presentation of Predicate Logic - (Extended Abstract). In FOSSACS 2013. doi:10.1007\/978-3-642-37075-5_26","DOI":"10.1007\/978-3-642-37075-5_26"},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","unstructured":"Sam Staton. 2013. Instances of Computational Effects: An Algebraic Perspective. In LICS 2013. doi:10.1109\/LICS.2013.58","DOI":"10.1109\/LICS.2013.58"},{"key":"e_1_3_2_45_2","doi-asserted-by":"publisher","unstructured":"Sam Staton. 2015. Algebraic Effects Linearity and Quantum Programming Languages. In POPL 2015. doi:10.1145\/2676726.2676999","DOI":"10.1145\/2676726.2676999"},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","unstructured":"W. W. Tait. 1967. Intensional interpretations of functionals of finite type I. Journal of Symbolic Logic 32 2 (1967) 198\u2013212. doi:10.2307\/2271658","DOI":"10.2307\/2271658"},{"key":"e_1_3_2_47_2","doi-asserted-by":"publisher","unstructured":"Aaron Joseph Turon and Mitchell Wand. 2011. A separation logic for refining concurrent objects. In POPL. ACM. doi:10.1145\/1926385.1926415","DOI":"10.1145\/1926385.1926415"},{"key":"e_1_3_2_48_2","doi-asserted-by":"publisher","unstructured":"Rob J. van Glabbeek and Gordon D. Plotkin. 2010. On CSP and the Algebraic Theory of Effects. In Reflections on the Work of C. A. R. Hoare A. W. Roscoe Clifford B. Jones and Kenneth R. Wood (Eds.). Springer 333\u2013369. doi:10.1007\/978-1-84882-912-1_15","DOI":"10.1007\/978-1-84882-912-1_15"},{"key":"e_1_3_2_49_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211617"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/dl.acm.org\/doi\/pdf\/10.1145\/3776706","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T13:44:57Z","timestamp":1784209497000},"score":1,"resource":{"primary":{"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/dl.acm.org\/doi\/10.1145\/3776706"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,1,8]]},"references-count":48,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2026,1,8]]}},"alternative-id":["10.1145\/3776706"],"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1145\/3776706","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,1,8]]},"assertion":[{"value":"2025-07-10","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-11-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-01-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}