{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,13]],"date-time":"2026-03-13T19:12:51Z","timestamp":1773429171625,"version":"3.50.1"},"publisher-location":"Singapore","reference-count":18,"publisher":"Springer Nature Singapore","isbn-type":[{"value":"9789819535842","type":"print"},{"value":"9789819535859","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,10,31]],"date-time":"2025-10-31T00:00:00Z","timestamp":1761868800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,10,31]],"date-time":"2025-10-31T00:00:00Z","timestamp":1761868800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-981-95-3585-9_1","type":"book-chapter","created":{"date-parts":[[2025,10,30]],"date-time":"2025-10-30T06:06:25Z","timestamp":1761804385000},"page":"3-21","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Memory Safety: Uniqueness as\u00a0Separation"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8884-618X","authenticated-orcid":false,"given":"Pilar Selene","family":"Linares Ar\u00e9valo","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9916-6614","authenticated-orcid":false,"given":"Arthur","family":"Azevedo de Amorim","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8737-4202","authenticated-orcid":false,"given":"Vincent","family":"Jackson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2765-4269","authenticated-orcid":false,"given":"Liam","family":"O\u2019Connor","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5959-3769","authenticated-orcid":false,"given":"Peter","family":"Schachte","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4785-2836","authenticated-orcid":false,"given":"Christine","family":"Rizkallah","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,10,31]]},"reference":[{"key":"1_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/978-3-319-89722-6_4","volume-title":"Principles of Security and Trust","author":"A Azevedo de Amorim","year":"2018","unstructured":"Azevedo de Amorim, A., Hri\u0163cu, C., Pierce, B.C.: The meaning of memory safety. In: Bauer, L., K\u00fcsters, R. (eds.) POST 2018. LNCS, vol. 10804, pp. 79\u2013105. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89722-6_4"},{"key":"1_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/3-540-57529-4_42","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"E Barendsen","year":"1993","unstructured":"Barendsen, E., Smetsers, S.: Conventional and uniqueness typing in graph rewrite systems. In: Shyamasundar, R.K. (ed.) FSTTCS 1993. LNCS, vol. 761, pp. 41\u201351. Springer, Heidelberg (1993). https:\/\/doi.org\/10.1007\/3-540-57529-4_42"},{"key":"1_CR3","doi-asserted-by":"publisher","unstructured":"Brady, E.C.: Type-driven development of concurrent communicating systems. Comput. Sci. 18(3) (2017). https:\/\/doi.org\/10.7494\/CSCI.2017.18.3.1413","DOI":"10.7494\/CSCI.2017.18.3.1413"},{"key":"1_CR4","doi-asserted-by":"publisher","unstructured":"Cheung, L., O\u2019Connor, L., Rizkallah, C.: Overcoming restraint: composing verification of foreign functions with cogent. In: Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2022, pp. 13\u201326. Association for Computing Machinery, New York, NY, USA (2022). https:\/\/doi.org\/10.1145\/3497775.3503686","DOI":"10.1145\/3497775.3503686"},{"key":"1_CR5","unstructured":"Herhut, S.B.S.S., Penczek, F., Grelck, C., Shinkarov, A., Viessmann, H.N.: Single assignment C tutorial (2025)"},{"key":"1_CR6","doi-asserted-by":"publisher","unstructured":"Jung, R.: Understanding and evolving the Rust programming language. Ph.D. thesis, Universit\u00e4t des Saarlandes (2020). https:\/\/doi.org\/10.22028\/D291-31946","DOI":"10.22028\/D291-31946"},{"key":"1_CR7","doi-asserted-by":"publisher","unstructured":"Jung, R., Jourdan, J.H., Krebbers, R., Dreyer, D.: RustBelt: securing the foundations of the rust programming language. Proc. ACM Program. Lang. 2(POPL) (2017). https:\/\/doi.org\/10.1145\/3158154","DOI":"10.1145\/3158154"},{"key":"1_CR8","unstructured":"McCarthy, J., Hayes, P.: Some philosophical problems from the standpoint of artificial intelligence. In: Meltzer, B., Michie, D. (eds.) Machine Intelligence, vol. 4, pp. 463\u2013502. Edinburgh University Press (1969)"},{"key":"1_CR9","doi-asserted-by":"crossref","unstructured":"O\u2019Connor, L., et al.: Refinement through restraint: bringing down the cost of verification (2016)","DOI":"10.1145\/2951913.2951940"},{"key":"1_CR10","doi-asserted-by":"publisher","DOI":"10.1017\/S095679682100023X","volume":"31","author":"L O\u2019Connor","year":"2021","unstructured":"O\u2019Connor, L., et al.: Cogent: uniqueness types and certifying compilation. J. Funct. Program. 31, e25 (2021). https:\/\/doi.org\/10.1017\/S095679682100023X","journal-title":"J. Funct. Program."},{"key":"1_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44802-0_1","volume-title":"Computer Science Logic","author":"P O\u2019Hearn","year":"2001","unstructured":"O\u2019Hearn, P., Reynolds, J., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001. LNCS, vol. 2142, pp. 1\u201319. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44802-0_1"},{"key":"1_CR12","doi-asserted-by":"publisher","unstructured":"O\u2019Hearn, P.W.: Resources, concurrency, and local reasoning. Theore. Comput. Sci. 375(1), 271\u2013307 (2007). https:\/\/doi.org\/10.1016\/j.tcs.2006.12.035. https:\/\/www.sciencedirect.com\/science\/article\/pii\/S030439750600925X. festschrift for John C. Reynolds\u2019s 70th birthday","DOI":"10.1016\/j.tcs.2006.12.035"},{"key":"1_CR13","doi-asserted-by":"publisher","unstructured":"Patterson, D., Mushtak, N., Wagner, A., Ahmed, A.: Semantic soundness for language interoperability. In: Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2022, pp. 609\u2013624. Association for Computing Machinery, New York, NY, USA (2022). https:\/\/doi.org\/10.1145\/3519939.3523703","DOI":"10.1145\/3519939.3523703"},{"key":"1_CR14","doi-asserted-by":"publisher","unstructured":"Reynolds, J.: Separation logic: a logic for shared mutable data structures. In: Proceedings 17th Annual IEEE Symposium on Logic in Computer Science, pp. 55\u201374. IEEE (2002). https:\/\/doi.org\/10.1109\/LICS.2002.1029817","DOI":"10.1109\/LICS.2002.1029817"},{"key":"1_CR15","unstructured":"Rinus\u00a0Plasmeijer, van\u00a0Eekelen, M.: Clean version 2.2 language report. Language report (2011)"},{"issue":"6","key":"1_CR16","doi-asserted-by":"publisher","first-page":"1005","DOI":"10.1017\/S0956796802004458","volume":"13","author":"SB Scholz","year":"2003","unstructured":"Scholz, S.B.: Single assignment C: efficient support for high-level array operations in a functional setting. J. Funct. Program. 13(6), 1005\u20131059 (2003)","journal-title":"J. Funct. Program."},{"key":"1_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"358","DOI":"10.1007\/3-540-57787-4_23","volume-title":"Graph Transformations in Computer Science","author":"S Smetsers","year":"1994","unstructured":"Smetsers, S., Barendsen, E., van Eekelen, M., Plasmeijer, R.: Guaranteeing safe destructive updates through a type system with uniqueness information for graphs. In: Schneider, H.J., Ehrig, H. (eds.) Graph Transformations in Computer Science. LNCS, vol. 776, pp. 358\u2013379. Springer, Heidelberg (1994). https:\/\/doi.org\/10.1007\/3-540-57787-4_23"},{"key":"1_CR18","doi-asserted-by":"publisher","unstructured":"Somogyi, Z., Henderson, F., Conway, T.C.: The execution algorithm of mercury, an efficient purely declarative logic programming language. J. Log. Program. 29(1-3), 17\u201364 (1996). https:\/\/doi.org\/10.1016\/S0743-1066(96)00068-4","DOI":"10.1016\/S0743-1066(96)00068-4"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-981-95-3585-9_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,13]],"date-time":"2026-03-13T18:13:41Z","timestamp":1773425621000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-981-95-3585-9_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,31]]},"ISBN":["9789819535842","9789819535859"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-981-95-3585-9_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,10,31]]},"assertion":[{"value":"31 October 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"APLAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Asian Symposium on Programming Languages and Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Bengaluru","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"India","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":"27 June 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 June 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"aplas2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/track\/aplas-2025\/aplas-2025-aplas-2025","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}