{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T21:06:27Z","timestamp":1760043987645,"version":"3.41.0"},"reference-count":21,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2023,10,16]],"date-time":"2023-10-16T00:00:00Z","timestamp":1697414400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2023,10,16]]},"abstract":"<jats:p>Reference immutability is a type based technique for taming mutation that has long been studied in the  \ncontext of object-oriented languages, like Java. Recently, though, languages like Scala have blurred the lines  \nbetween functional programming languages and object oriented programming languages. We explore how  \nreference immutability interacts with features commonly found in these hybrid languages, in particular with  \nhigher-order functions \u2013 polymorphism \u2013 and subtyping. We construct a calculus System F&lt;:M which encodes  \na reference immutability system as a simple extension of System F&lt;: and prove that it satisfies the standard  \nsoundness and immutability safety properties.<\/jats:p>","DOI":"10.1145\/3622828","type":"journal-article","created":{"date-parts":[[2023,10,16]],"date-time":"2023-10-16T15:41:29Z","timestamp":1697470889000},"page":"857-881","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Simple Reference Immutability for System F\n            <sub>&lt;:<\/sub>"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7057-0912","authenticated-orcid":false,"given":"Edward","family":"Lee","sequence":"first","affiliation":[{"name":"University of Waterloo, Waterloo, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9066-1889","authenticated-orcid":false,"given":"Ond\u0159ej","family":"Lhot\u00e1k","sequence":"additional","affiliation":[{"name":"University of Waterloo, Waterloo, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,10,16]]},"reference":[{"volume-title":"The essence of dependent object types. A List of Successes That Can Change the World: Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday ( 2016 ), 249-272","author":"Amin Nada","key":"e_1_2_1_1_1","unstructured":"Nada Amin , Samuel Gr\u00fctter , Martin Odersky , Tiark Rompf , and Sandro Stucki . 2016. The essence of dependent object types. A List of Successes That Can Change the World: Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday ( 2016 ), 249-272 . Nada Amin, Samuel Gr\u00fctter, Martin Odersky, Tiark Rompf, and Sandro Stucki. 2016. The essence of dependent object types. A List of Successes That Can Change the World: Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday ( 2016 ), 249-272."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328443"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3386323"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-54415-1_73"},{"key":"e_1_2_1_5_1","first-page":"28","volume-title":"Generic Universe Types. In ECOOP 2007-Object-Oriented Programming, Erik Ernst (Ed.). Springer Berlin Heidelberg","author":"Dietl Werner","year":"2007","unstructured":"Werner Dietl , Sophia Drossopoulou , and Peter M\u00fcller . 2007 . Generic Universe Types. In ECOOP 2007-Object-Oriented Programming, Erik Ernst (Ed.). Springer Berlin Heidelberg , Berlin, Heidelberg , 28 - 53 . Werner Dietl, Sophia Drossopoulou, and Peter M\u00fcller. 2007. Generic Universe Types. In ECOOP 2007-Object-Oriented Programming, Erik Ernst (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 28-53."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429104"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2020.18"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/41625.41654"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/301618.301665"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384619"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.4204\/eptcs.246.5"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384680"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/503502.503505"},{"key":"e_1_2_1_14_1","unstructured":"Edward Lee and Ond\u0159ej Lhot\u00e1k. 2023a. Artifact for the OOPSLA 2023 paper 'Simple Reference Immutability for System Fsub'. https:\/\/archive.softwareheritage.org\/swh:1:rev:709bb054f0eb4a891c9c54065a255df0a360800;origin=https:\/\/github. com\/e45lee\/simple-fsub-mutability-proofs;visit=swh:1:snp:04d537961ccf54bc85606d60b180c2e8083b14ba \t\t\t\t  Edward Lee and Ond\u0159ej Lhot\u00e1k. 2023a. Artifact for the OOPSLA 2023 paper 'Simple Reference Immutability for System Fsub'. https:\/\/archive.softwareheritage.org\/swh:1:rev:709bb054f0eb4a891c9c54065a255df0a360800;origin=https:\/\/github. com\/e45lee\/simple-fsub-mutability-proofs;visit=swh:1:snp:04d537961ccf54bc85606d60b180c2e8083b14ba"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3580414"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276482"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-4118-8_9"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384685"},{"volume-title":"The C+ + programming language-special edition (3. ed.)","author":"Stroustrup Bjarne","key":"e_1_2_1_19_1","unstructured":"Bjarne Stroustrup . 2007. The C+ + programming language-special edition (3. ed.) . Addison-Wesley . Bjarne Stroustrup. 2007. The C+ + programming language-special edition (3. ed.). Addison-Wesley."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1094811.1094828"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1287624.1287637"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3622828","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3622828","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:37:04Z","timestamp":1750178224000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3622828"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,10,16]]},"references-count":21,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2023,10,16]]}},"alternative-id":["10.1145\/3622828"],"URL":"https:\/\/doi.org\/10.1145\/3622828","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2023,10,16]]},"assertion":[{"value":"2023-10-16","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}