{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T00:41:54Z","timestamp":1767919314695,"version":"3.49.0"},"reference-count":44,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","funder":[{"name":"Funda\u00e7\u00e3o para a Ci\u00eancia e a Tecnologia, I.P","award":["UID\/50021\/2025"],"award-info":[{"award-number":["UID\/50021\/2025"]}]},{"name":"Funda\u00e7\u00e3o para a Ci\u00eancia e a Tecnologia, I.P","award":["UID\/PRR\/50021\/2025"],"award-info":[{"award-number":["UID\/PRR\/50021\/2025"]}]}],"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>Traditionally, in linearly typed languages, consuming a linear resource is synonymous with its syntactic occurrence in the program. However, under the lens of non-strict evaluation, linearity can be further understood semantically, where a syntactic occurrence of a resource does not necessarily entail using that resource when the program is executed. While this distinction has been largely unexplored, it turns out to be inescapable in Haskell's optimising compiler, which heavily rewrites the source program in ways that break syntactic linearity but preserve the program's semantics. We introduce Linear Core, a novel system which accepts the lazy semantics of linearity statically and is suitable for lazy languages such as the Core intermediate language of the Glasgow Haskell Compiler. We prove that Linear Core is sound, guaranteeing linear resource usage, and that multiple optimising transformations preserve linearity in Linear Core while failing to do so in Core. We have implemented Linear Core as a compiler plugin to validate the system against linearity-heavy libraries, including linear-base.<\/jats:p>","DOI":"10.1145\/3776711","type":"journal-article","created":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T18:59:43Z","timestamp":1767898783000},"page":"1994-2020","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Lazy Linearity for a Core Functional Language"],"prefix":"10.1145","volume":"10","author":[{"ORCID":"https:\/\/orcid.org\/0009-0005-1467-115X","authenticated-orcid":false,"given":"Rodrigo","family":"Mesquita","sequence":"first","affiliation":[{"name":"Well-Typed LLP, London, United Kingdom"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0746-7514","authenticated-orcid":false,"given":"Bernardo","family":"Toninho","sequence":"additional","affiliation":[{"name":"Instituto Superior T\u00e9cnico, University of Lisbon, Lisbon, Portugal"},{"name":"INESC-ID, Lisbon, Portugal"}]}],"member":"320","published-online":{"date-parts":[[2026,1,8]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/2.3.297"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796803004751"},{"key":"e_1_2_2_3_1","volume-title":"Dual Intuitionistic Linear Logic","author":"Barber Andrew","unstructured":"Andrew Barber. 1996. Dual Intuitionistic Linear Logic. The University of Edinburgh."},{"key":"e_1_2_2_4_1","volume-title":"Simon Peyton Jones, and Arnaud Spiwack","author":"Bernardy Jean-Philippe","year":"2017","unstructured":"Jean-Philippe Bernardy, Mathieu Boespflug, Ryan R. Newton, Simon Peyton Jones, and Arnaud Spiwack. 2017. Linear Haskell: practical linearity in a higher-order polymorphic language. CoRR, abs\/1710.09756 (2017), arXiv:1710.09756. arxiv:1710.09756"},{"key":"e_1_2_2_5_1","unstructured":"J. Bernardy R. Eisenberg M. Boespflug R. Newton S. Peyton Jones and A. Spiwack. 2020. Linear Mini-Core. https:\/\/gitlab.haskell.org\/ghc\/ghc\/-\/wikis\/uploads\/355cd9a03291a852a518b0cb42f960b4\/minicore.pdf"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158093"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3471874.3472980"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/1760267.1760273"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2021.9"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.5445\/IR\/1000054251"},{"key":"e_1_2_2_11_1","doi-asserted-by":"crossref","unstructured":"T. H. Brus M. C. J. D. van Eekelen M. O. van Leer and M. J. Plasmeijer. 1987. Clean \u2014 A language for functional graph rewriting. In Functional Programming Languages and Computer Architecture Gilles Kahn (Ed.). Springer Berlin Heidelberg Berlin Heidelberg. 364\u2013384. isbn:978-3-540-47879-9","DOI":"10.1007\/3-540-18317-5_20"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15375-4_16"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)00173-5"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800001660"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434331"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1291151.1291199"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/582153.582176"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.2307\/2275431"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3373718.3394765"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/165180.165214"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3471874.3472979"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/158511.158618"},{"key":"e_1_2_2_24_1","unstructured":"Andrew Lelechenko. 2024. text-builder-linear: Builder for Text and ByteString based on linear types. https:\/\/hackage.haskell.org\/package\/text-builder-linear"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3527313"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99336-8_13"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2692956.2663188"},{"key":"e_1_2_2_28_1","volume-title":"ACM Conference on Programming Languages Design and Implementation (PLDI\u201917)","author":"Maurer Luke","year":"2017","unstructured":"Luke Maurer, Zena Ariola, Paul Downen, and Simon Peyton Jones. 2017. Compiling without continuations. In ACM Conference on Programming Languages Design and Implementation (PLDI\u201917). ACM, 482\u2013494. https:\/\/www.microsoft.com\/en-us\/research\/publication\/compiling-without-continuations\/"},{"key":"e_1_2_2_29_1","volume-title":"Lazy Linearity for a Core Functional Language. CoRR, abs\/2511.10361","author":"Mesquita Rodrigo","year":"2025","unstructured":"Rodrigo Mesquita and Bernardo Toninho. 2025. Lazy Linearity for a Core Functional Language. CoRR, abs\/2511.10361 (2025), arXiv:2511.10361. arxiv:2511.10361"},{"key":"e_1_2_2_30_1","volume-title":"Linear Core: Theory and a GHC Plugin. https:\/\/hackage.haskell.org\/package\/linear-core-prototype-0.1.0.0","author":"Mesquita Rodrigo","year":"2025","unstructured":"Rodrigo Mesquita and Bernardo Toninho. 2025. Linear Core: Theory and a GHC Plugin. https:\/\/hackage.haskell.org\/package\/linear-core-prototype-0.1.0.0"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796802004331"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/232629.232630"},{"key":"e_1_2_2_33_1","volume-title":"A transformation-based optimiser for Haskell. Science of Computer Programming, 32, 1","author":"Jones Simon Peyton","year":"1997","unstructured":"Simon Peyton Jones and Andre Santos. 1997. A transformation-based optimiser for Haskell. Science of Computer Programming, 32, 1 (1997), October, https:\/\/www.microsoft.com\/en-us\/research\/publication\/a-transformation-based-optimiser-for-haskell\/"},{"key":"e_1_2_2_34_1","volume-title":"The Implementation of Functional Programming Languages","author":"Peyton Jones Simon L.","unstructured":"Simon L. Peyton Jones. 1987. The Implementation of Functional Programming Languages (Prentice-Hall International Series in Computer Science). Prentice-Hall, Inc., USA. isbn:013453333X"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3331545.3342599"},{"key":"e_1_2_2_36_1","volume-title":"Advanced Topics in Types and Programming Languages","author":"Pierce Benjamin C.","unstructured":"Benjamin C. Pierce. 2004. Advanced Topics in Types and Programming Languages. The MIT Press. isbn:0262162288"},{"key":"e_1_2_2_37_1","unstructured":"Andre Santos and Simon Peyton Jones. 1995. Compilation by transformation for non-strict functional languages. Ph. D. Dissertation. https:\/\/www.microsoft.com\/en-us\/research\/publication\/compilation-transformation-non-strict-functional-languages\/"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796817000016"},{"key":"e_1_2_2_39_1","unstructured":"Arnaud Spiwack David Feuer and Jos\u00e9 Pedro Magalh\u00e3es. 2025. linear-generics: Generic programming library for generalised deriving. https:\/\/hackage.haskell.org\/package\/linear-generics"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547626"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190315.1190324"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","unstructured":"Bernardo Toninho and Rodrigo Mesquita. 2025. Lazy Linearity for a Core Functional Language (Artifact). https:\/\/doi.org\/10.5281\/zenodo.17713905 10.5281\/zenodo.17713905","DOI":"10.5281\/zenodo.17713905"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)00054-7"},{"key":"e_1_2_2_44_1","unstructured":"Philip Wadler. 1990. Linear Types can Change the World!. In Programming Concepts and Methods."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3776711","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T19:03:48Z","timestamp":1767899028000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3776711"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,1,8]]},"references-count":44,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2026,1,8]]}},"alternative-id":["10.1145\/3776711"],"URL":"https:\/\/doi.org\/10.1145\/3776711","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"}}]}}