{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,15]],"date-time":"2025-08-15T00:27:41Z","timestamp":1755217661570,"version":"3.43.0"},"reference-count":42,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","funder":[{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["NN66001-22-C-4027"],"award-info":[{"award-number":["NN66001-22-C-4027"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000038","name":"Natural Sciences and Engineering Research Council of Canada","doi-asserted-by":"publisher","award":["RGPIN-2019-04207"],"award-info":[{"award-number":["RGPIN-2019-04207"]}],"id":[{"id":"10.13039\/501100000038","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,8,5]]},"abstract":"<jats:p>What are mutable references; what do they mean? The answers to these questions have spawned lots of important theoretical work and form the foundation of many impactful tools. However, existing semantics collapse a key distinction: which allocations does a reference depend on?<\/jats:p>\n          <jats:p>In this paper, we deconstruct the space of mutable higher-order references. We formalize a novel distinction\u2014splitting the design space of references not only into higher-order vs (full-)ground references, but also dependency of an allocation on past vs future allocations. This distinction is fundamental to a thorny issue that arises in constructing semantic models of mutable references\u2014the type-world circularity. The issue disappears for what we call predicative references, those that only quantify over past, not future, allocations, and for non-higher-order impredicative references. We design a syntax and semantics for each point in our newly described space. The syntax relies on a type universe hierarchy, \u00e0 la dependent type theory, to kind the types of allocated terms, and stratify allocations. Each type universe corresponds to a semantic Kripke world, giving a lightweight syntactic mechanism to design and restrict heap shapes. The semantics bear a resemblance to work on regions, and suggest some connection between universe systems and regions, which we describe in some detail.<\/jats:p>","DOI":"10.1145\/3747532","type":"journal-article","created":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T16:56:02Z","timestamp":1754412962000},"page":"784-813","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Type Universes as Kripke Worlds"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0325-3305","authenticated-orcid":false,"given":"Paulette","family":"Koronkevich","sequence":"first","affiliation":[{"name":"University of British Columbia, Vancouver, Canada"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6402-4840","authenticated-orcid":false,"given":"William J.","family":"Bowman","sequence":"additional","affiliation":[{"name":"University of British Columbia, Vancouver, Canada"}]}],"member":"320","published-online":{"date-parts":[[2025,8,5]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1998.705669"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009878"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480925"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/11417170_22"},{"key":"e_1_2_2_5_1","unstructured":"Amal Jamil Ahmed. 2004. Semantics of Types for Mutable State. Ph. D. Dissertation. https:\/\/www.cs.princeton.edu\/techreports\/2004\/713.pdf"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10672-9_16"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/504709.504712"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190235"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3622846"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","unstructured":"Yuyan Bao Songlin Jia Guannan Wei Oliver Bra\u010devac and Tiark Rompf. 2023. Modeling Reachability Types with Logical Relations. https:\/\/doi.org\/10.48550\/ARXIV.2309.05885 10.48550\/ARXIV.2309.05885","DOI":"10.48550\/ARXIV.2309.05885"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485516"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/11417170_8"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3618003"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74407-8_19"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2009.06.007"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-91118-7_10"},{"volume-title":"Advanced Topics in Types and Programming Languages, Benjamin C","author":"Crary Karl","key":"e_1_2_2_17_1","unstructured":"Karl Crary. 2005. Logical Relations and a Case Study in Equivalence Checking. In Advanced Topics in Types and Programming Languages, Benjamin C. Pierce (Ed.). MIT Press, Chapter 6."},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-92188-2_4"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15375-4_23"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","unstructured":"Romain Demangeon Daniel Hirschkoff and Davide Sangiorgi. 2012. Strong Normalisation in lambda-Calculi with References. In Fundamentals of Software Engineering (FSEN). https:\/\/doi.org\/10.1007\/978-3-642-29320-7_9 10.1007\/978-3-642-29320-7_9","DOI":"10.1007\/978-3-642-29320-7_9"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.5381\/jot.2005.4.8.a1"},{"key":"e_1_2_2_22_1","unstructured":"Jean-Yves Girard. 1972. Interpr\u00e9tation fonctionelle et \u00e9limination des coupures de l\u2019arithm\u00e9tique d\u2019ordre sup\u00e9rieur. Ph. D. Dissertation. Universit\u00e9 Paris VII. https:\/\/www.worldcat.org\/oclc\/493768392"},{"key":"e_1_2_2_23_1","unstructured":"Ernest Hemingway. 1926. The Sun Also Rises. Scribner."},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571250"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/lics.2017.8005109"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/6.4.308"},{"key":"e_1_2_2_27_1","unstructured":"Paul Blain Levy. 2001. Call-by-push-value. Ph. D. Dissertation. Queen Mary University of London UK. https:\/\/pblevy.github.io\/papers\/thesisqmwphd.pdf"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45793-3_16"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.10.015"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3674642"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/s0049-237x(08)71945-1"},{"key":"e_1_2_2_32_1","unstructured":"Conor McBride. [n. d.]. Crude but Effective Stratification. https:\/\/mazzo.li\/epilogue\/index.html Accessed on 2025-02-01."},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523443"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31585-5_30"},{"volume-title":"Types and Programming Languages","author":"Pierce Benjamin C.","key":"e_1_2_2_35_1","unstructured":"Benjamin C. Pierce. 2002. Types and Programming Languages. MIT Press Ltd. isbn:0-262-16209-1"},{"volume-title":"Operational reasoning for functions with local state","author":"Pitts Andrew","key":"e_1_2_2_36_1","unstructured":"Andrew Pitts and Ian Stark. 1999. Operational reasoning for functions with local state. Cambridge University Press, 227\u2013274."},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371126"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034811"},{"key":"e_1_2_2_39_1","unstructured":"The Swift Development Team. [n. d.]. Swift Language Documentation: Strong Reference Cycles for Closures. https:\/\/docs.swift.org\/swift-book\/documentation\/the-swift-programming-language\/automaticreferencecounting\/#Strong-Reference-Cycles-for-Closures Accessed on 2025-02-01."},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.2613"},{"key":"e_1_2_2_41_1","unstructured":"Paolo Tranquilli. 2011. Termination of Threads with Shared Memory via Infinitary Choice. (2011). https:\/\/hal.science\/hal-00573690"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632856"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3747532","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T16:56:10Z","timestamp":1754412970000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3747532"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,8,5]]},"references-count":42,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2025,8,5]]}},"alternative-id":["10.1145\/3747532"],"URL":"https:\/\/doi.org\/10.1145\/3747532","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2025,8,5]]},"assertion":[{"value":"2025-02-27","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-06-27","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-08-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}