{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,11]],"date-time":"2026-06-11T02:07:11Z","timestamp":1781143631046,"version":"3.54.1"},"publisher-location":"Cham","reference-count":65,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030993351","type":"print"},{"value":"9783030993368","type":"electronic"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T00:00:00Z","timestamp":1648512000000},"content-version":"vor","delay-in-days":87,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Substructural type systems are growing in popularity because they allow for a resourceful interpretation of data which can be used to rule out various software bugs. Indeed, substructurality is finally taking hold in modern programming; Haskell now has linear types roughly based on Girard\u2019s linear logic but integrated via graded function arrows, Clean has uniqueness types designed to ensure that values have at most a single reference to them, and Rust has an intricate ownership system for guaranteeing memory safety. But despite this broad range of resourceful type systems, there is comparatively little understanding of their relative strengths and weaknesses or whether their underlying frameworks can be unified. There is often confusion about whether linearity and uniqueness are essentially the same, or are instead \u2018dual\u2019 to one another, or somewhere in between. This paper formalises the relationship between these two well-studied but rarely contrasted ideas, building on two distinct bodies of literature, showing that it is possible and advantageous to have both linear and unique types in the same type system. We study the guarantees of the resulting system and provide a practical implementation in the graded modal setting of the Granule language, adding a third kind of modality alongside coeffect and effect modalities. We then demonstrate via a benchmark that our implementation benefits from expected efficiency gains enabled by adding uniqueness to a language that already has a linear basis.<\/jats:p>","DOI":"10.1007\/978-3-030-99336-8_13","type":"book-chapter","created":{"date-parts":[[2022,3,28]],"date-time":"2022-03-28T20:02:48Z","timestamp":1648497768000},"page":"346-375","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["Linearity and Uniqueness: An Entente Cordiale"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4284-3757","authenticated-orcid":false,"given":"Danielle","family":"Marshall","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0496-8268","authenticated-orcid":false,"given":"Michael","family":"Vollmer","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7058-7842","authenticated-orcid":false,"given":"Dominic","family":"Orchard","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2022,3,29]]},"reference":[{"key":"13_CR1","doi-asserted-by":"publisher","unstructured":"Ahrens, B., Spadotti, R.: Terminal semantics for codata types in intensional Martin-L\u00f6f type theory. In: Herbelin, H., Letouzey, P., Sozeau, M. (eds.) 20th International Conference on Types for Proofs and Programs (TYPES 2014). Leibniz International Proceedings in Informatics (LIPIcs), vol. 39, pp. 1\u201326. Schloss Dagstuhl, Germany (Oct 2015). https:\/\/doi.org\/10.4230\/LIPIcs.TYPES.2014.1","DOI":"10.4230\/LIPIcs.TYPES.2014.1"},{"key":"13_CR2","doi-asserted-by":"publisher","unstructured":"Aldrich, J., Kostadinov, V., Chambers, C.: Alias annotations for program understanding. In: Proceedings of the 17th ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications. p. 311\u2013330. OOPSLA \u201902, Association for Computing Machinery, New York, NY, USA (2002). https:\/\/doi.org\/10.1145\/582419.582448","DOI":"10.1145\/582419.582448"},{"key":"13_CR3","doi-asserted-by":"publisher","unstructured":"Altenkirch, T., Chapman, J., Uustalu, T.: Monads need not be endofunctors. Logical Methods in Computer Science 11(1) (Mar 2015). https:\/\/doi.org\/10.2168\/lmcs-11(1:3)2015","DOI":"10.2168\/lmcs-11(1:3)2015"},{"key":"13_CR4","doi-asserted-by":"publisher","unstructured":"Baker, H.G.: Lively linear Lisp: \u201clook ma, no garbage!\". SIGPLAN Not. 27(8), 89\u201398 (Aug 1992). https:\/\/doi.org\/10.1145\/142137.142162","DOI":"10.1145\/142137.142162"},{"key":"13_CR5","doi-asserted-by":"crossref","unstructured":"Barendsen, E., Smetsers, S.: Conventional and uniqueness typing in graph rewrite systems. In: International Conference on Foundations of Software Technology and Theoretical Computer Science. pp. 41\u201351. Springer (1993)","DOI":"10.1007\/3-540-57529-4_42"},{"key":"13_CR6","doi-asserted-by":"crossref","unstructured":"Benton, P.N.: A mixed linear and non-linear logic: Proofs, terms and models. In: Pacholski, L., Tiuryn, J. (eds.) Computer Science Logic. pp. 121\u2013135. Springer Berlin Heidelberg, Berlin, Heidelberg (1995)","DOI":"10.1007\/BFb0022251"},{"key":"13_CR7","doi-asserted-by":"publisher","unstructured":"Bernardy, J.P., Boespflug, M., Newton, R.R., Peyton Jones, S., Spiwack, A.: Linear Haskell: Practical linearity in a higher-order polymorphic language. Proc. ACM Program. Lang. 2(POPL) (Dec 2017). https:\/\/doi.org\/10.1145\/3158093","DOI":"10.1145\/3158093"},{"key":"13_CR8","doi-asserted-by":"crossref","unstructured":"Boyland, J.: Checking interference with fractional permissions. In: Cousot, R. (ed.) Static Analysis. pp. 55\u201372. Springer Berlin Heidelberg, Berlin, Heidelberg (2003)","DOI":"10.1007\/3-540-44898-5_4"},{"key":"13_CR9","doi-asserted-by":"publisher","unstructured":"Brady, E.: Idris 2: Quantitative Type Theory in Practice. In: M\u00f8ller, A., Sridharan, M. (eds.) 35th European Conference on Object-Oriented Programming (ECOOP 2021). Leibniz International Proceedings in Informatics (LIPIcs), vol. 194, pp. 9:1\u20139:26. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2021). https:\/\/doi.org\/10.4230\/LIPIcs.ECOOP.2021.9, https:\/\/drops.dagstuhl.de\/opus\/volltexte\/2021\/14052","DOI":"10.4230\/LIPIcs.ECOOP.2021.9"},{"key":"13_CR10","unstructured":"Bryant, A.B., Eades, H.D.: The graded Lambek calculus. In: 2020 Joint Workshop on Linearity & TLLA: The 6th Workshop on Linearity and the 4th Workshop on Trends in Linear Logic and Applications (2020), https:\/\/www.cs.unibo.it\/~dallago\/TLLALINEARITY2020\/The_Graded_Lambek_Calculus.pdf"},{"key":"13_CR11","doi-asserted-by":"crossref","unstructured":"Choudhury, P., Eades III, H., Eisenberg, R.A., Weirich, S.: A graded dependent type system with a usage-aware semantics. Proceedings of the ACM on Programming Languages 5(POPL), 1\u201332 (2021)","DOI":"10.1145\/3434331"},{"key":"13_CR12","doi-asserted-by":"publisher","unstructured":"Choudhury, V., Krishnaswami, N.: Recovering purity with comonads and capabilities. Proc. ACM Program. Lang. 4(ICFP), 111:1\u2013111:28 (2020). https:\/\/doi.org\/10.1145\/3408993","DOI":"10.1145\/3408993"},{"key":"13_CR13","doi-asserted-by":"publisher","unstructured":"Coutts, D., Leshchinskiy, R., Stewart, D.: Stream fusion: From lists to streams to nothing at all. In: Proceedings of the 12th ACM SIGPLAN International Conference on Functional Programming. p. 315\u2013326. ICFP \u201907, Association for Computing Machinery, New York, NY, USA (2007). https:\/\/doi.org\/10.1145\/1291151.1291199","DOI":"10.1145\/1291151.1291199"},{"key":"13_CR14","doi-asserted-by":"crossref","unstructured":"Fluet, M., Morrisett, G., Ahmed, A.: Linear regions are all you need. In: Sestoft, P. (ed.) Programming Languages and Systems. pp. 7\u201321. Springer Berlin Heidelberg, Berlin, Heidelberg (2006)","DOI":"10.1007\/11693024_2"},{"key":"13_CR15","doi-asserted-by":"publisher","unstructured":"Girard, J.Y.: Linear logic. Theoretical Computer Science 50(1), 1 \u2013 101 (1987). https:\/\/doi.org\/10.1016\/0304-3975(87)90045-4, http:\/\/www.sciencedirect.com\/science\/article\/pii\/0304397587900454","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"13_CR16","doi-asserted-by":"crossref","unstructured":"Girard, J.Y., Scedrov, A., Scott, P.J.: Bounded linear logic: a modular approach to polynomial-time computability. Theoretical computer science 97(1), 1\u201366 (1992)","DOI":"10.1016\/0304-3975(92)90386-T"},{"key":"13_CR17","doi-asserted-by":"publisher","unstructured":"Gordon, C.S.: Designing with Static Capabilities and Effects: Use, Mention, and Invariants (Pearl). In: Hirschfeld, R., Pape, T. (eds.) 34th European Conference on Object-Oriented Programming (ECOOP 2020). Leibniz International Proceedings in Informatics (LIPIcs), vol. 166, pp. 10:1\u201310:25. Schloss Dagstuhl\u2013Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2020). https:\/\/doi.org\/10.4230\/LIPIcs.ECOOP.2020.10, https:\/\/drops.dagstuhl.de\/opus\/volltexte\/2020\/13167","DOI":"10.4230\/LIPIcs.ECOOP.2020.10"},{"key":"13_CR18","doi-asserted-by":"publisher","unstructured":"Guzman, J., Hudak, P.: Single-threaded polymorphic lambda calculus. In: [1990] Proceedings. Fifth Annual IEEE Symposium on Logic in Computer Science. pp. 333\u2013343 (1990). https:\/\/doi.org\/10.1109\/LICS.1990.113759","DOI":"10.1109\/LICS.1990.113759"},{"key":"13_CR19","doi-asserted-by":"crossref","unstructured":"Haller, P., Odersky, M.: Capabilities for uniqueness and borrowing. In: D\u2019Hondt, T. (ed.) ECOOP 2010 \u2013 Object-Oriented Programming. pp. 354\u2013378. Springer Berlin Heidelberg, Berlin, Heidelberg (2010)","DOI":"10.1007\/978-3-642-14107-2_17"},{"key":"13_CR20","doi-asserted-by":"crossref","unstructured":"Harrington, D.: Uniqueness logic. Theoretical Computer Science 354(1), 24\u201341 (2006)","DOI":"10.1016\/j.tcs.2005.11.006"},{"key":"13_CR21","doi-asserted-by":"publisher","unstructured":"Hicks, M., Morrisett, G., Grossman, D., Jim, T.: Experience with safe manual memory-management in Cyclone. In: Proceedings of the 4th International Symposium on Memory Management. p. 73\u201384. ISMM \u201904, Association for Computing Machinery, New York, NY, USA (2004). https:\/\/doi.org\/10.1145\/1029873.1029883","DOI":"10.1145\/1029873.1029883"},{"key":"13_CR22","unstructured":"Hughes, J., Marshall, D., Wood, J., Orchard, D.: Linear Exponentials as Graded Modal Types. In: 5th International Workshop on Trends in Linear Logic and Applications (TLLA 2021). Rome (virtual), Italy (Jun 2021), https:\/\/hal-lirmm.ccsd.cnrs.fr\/lirmm-03271465"},{"key":"13_CR23","doi-asserted-by":"publisher","unstructured":"Jouvelot, P., Gifford, D.: Algebraic reconstruction of types and effects. In: Proceedings of the 18th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. p. 303\u2013310. POPL \u201991, Association for Computing Machinery, New York, NY, USA (1991). https:\/\/doi.org\/10.1145\/99583.99623","DOI":"10.1145\/99583.99623"},{"key":"13_CR24","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) (Dec 2017). https:\/\/doi.org\/10.1145\/3158154","DOI":"10.1145\/3158154"},{"key":"13_CR25","doi-asserted-by":"publisher","unstructured":"Keller, G., Chakravarty, M.M., Leshchinskiy, R., Peyton Jones, S., Lippmeier, B.: Regular, Shape-Polymorphic, Parallel Arrays in Haskell. In: Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming. p. 261\u2013272. ICFP \u201910, Association for Computing Machinery, New York, NY, USA (2010). https:\/\/doi.org\/10.1145\/1863543.1863582","DOI":"10.1145\/1863543.1863582"},{"key":"13_CR26","doi-asserted-by":"publisher","unstructured":"Lucassen, J.M., Gifford, D.K.: Polymorphic effect systems. In: Proceedings of the 15th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. p. 47\u201357. POPL \u201988, Association for Computing Machinery, New York, NY, USA (1988). https:\/\/doi.org\/10.1145\/73560.73564","DOI":"10.1145\/73560.73564"},{"key":"13_CR27","doi-asserted-by":"publisher","unstructured":"Mainland, G., Leshchinskiy, R., Peyton Jones, S.: Exploiting vector instructions with generalized stream fusion. In: Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming. p. 37\u201348. ICFP \u201913, Association for Computing Machinery, New York, NY, USA (2013). https:\/\/doi.org\/10.1145\/2500365.2500601","DOI":"10.1145\/2500365.2500601"},{"key":"13_CR28","doi-asserted-by":"publisher","unstructured":"Marshall, D., Vollmer, M., Orchard, D.: Linearity and Uniqueness: An Entente Cordiale (Appendix). https:\/\/doi.org\/10.5281\/zenodo.5919193","DOI":"10.5281\/zenodo.5919193"},{"key":"13_CR29","doi-asserted-by":"publisher","unstructured":"Marshall, D., Vollmer, M., Orchard, D.: Linearity and Uniqueness: An Entente Cordiale (Artifact). https:\/\/doi.org\/10.5281\/zenodo.5919209","DOI":"10.5281\/zenodo.5919209"},{"key":"13_CR30","doi-asserted-by":"publisher","unstructured":"McBride, C.: I Got Plenty o\u2019 Nuttin\u2019. In: A List of Successes That Can Change the World - Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday. pp. 207\u2013233 (2016). https:\/\/doi.org\/10.1007\/978-3-319-30936-1_12","DOI":"10.1007\/978-3-319-30936-1_12"},{"key":"13_CR31","doi-asserted-by":"crossref","unstructured":"Moon, B., Eades\u00a0III, H., Orchard, D.: Graded modal dependent type theory. In: Yoshida, N. (ed.) Programming Languages and Systems. pp. 462\u2013490. Springer International Publishing, Cham (2021)","DOI":"10.1007\/978-3-030-72019-3_17"},{"key":"13_CR32","doi-asserted-by":"publisher","unstructured":"Morris, J.G.: The Best of Both Worlds: Linear Functional Programming without Compromise. In: Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming. p. 448\u2013461. ICFP 2016, Association for Computing Machinery, New York, NY, USA (2016). https:\/\/doi.org\/10.1145\/2951913.2951925","DOI":"10.1145\/2951913.2951925"},{"key":"13_CR33","doi-asserted-by":"crossref","unstructured":"Morrisett, G., Ahmed, A., Fluet, M.: L$$^3$$: A linear language with locations. In: Urzyczyn, P. (ed.) Typed Lambda Calculi and Applications. pp. 293\u2013307. Springer Berlin Heidelberg, Berlin, Heidelberg (2005)","DOI":"10.1007\/11417170_22"},{"key":"13_CR34","doi-asserted-by":"publisher","unstructured":"Mycroft, A., Voigt, J.: Notions of aliasing and ownership. In: Clarke, D., Noble, J., Wrigstad, T. (eds.) Aliasing in Object-Oriented Programming. Types, Analysis and Verification, Lecture Notes in Computer Science, vol. 7850, pp. 59\u201383. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-36946-9_4","DOI":"10.1007\/978-3-642-36946-9_4"},{"key":"13_CR35","doi-asserted-by":"crossref","unstructured":"O\u2019Connor, L., Chen, Z., Rizkallah, C., Jackson, V., Amani, S., Klein, G., Murray, T., Sewell, T., Keller, G.: Cogent: Uniqueness types and certified compilation. J. Funct. Program. (2021)","DOI":"10.1017\/S095679682100023X"},{"key":"13_CR36","doi-asserted-by":"publisher","unstructured":"Orchard, D., Liepelt, V.B., Eades III, H.: Quantitative Program Reasoning with Graded Modal Types. Proc. ACM Program. Lang. 3(ICFP) (Jul 2019). https:\/\/doi.org\/10.1145\/3341714","DOI":"10.1145\/3341714"},{"key":"13_CR37","unstructured":"Orchard, D., Mycroft, A.: Categorical programming for data types with restricted parametricity. Unpublished note. (2012), https:\/\/www.cs.kent.ac.uk\/people\/staff\/dao7\/drafts\/tfp-structures-orchard12.pdf"},{"key":"13_CR38","doi-asserted-by":"publisher","unstructured":"Paykin, J., Zdancewic, S.: The linearity monad. In: Proceedings of the 10th ACM SIGPLAN International Symposium on Haskell. p. 117\u2013132. Haskell 2017, Association for Computing Machinery, New York, NY, USA (2017). https:\/\/doi.org\/10.1145\/3122955.3122965","DOI":"10.1145\/3122955.3122965"},{"key":"13_CR39","doi-asserted-by":"publisher","unstructured":"Pearce, D.J.: A lightweight formalism for reference lifetimes and borrowing in Rust. ACM Trans. Program. Lang. Syst. 43(1) (Apr 2021). https:\/\/doi.org\/10.1145\/3443420","DOI":"10.1145\/3443420"},{"key":"13_CR40","unstructured":"Plasmeijer, R., van Eekelen, M., van Groningen, J.: Clean Version 2.2 Language Report (2011), https:\/\/clean.cs.ru.nl\/download\/doc\/CleanLangRep.2.2.pdf"},{"key":"13_CR41","doi-asserted-by":"publisher","unstructured":"Pottier, F., Protzenko, J.: Programming with permissions in Mezzo. In: Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming. p. 173\u2013184. ICFP \u201913, Association for Computing Machinery, New York, NY, USA (2013). https:\/\/doi.org\/10.1145\/2500365.2500598","DOI":"10.1145\/2500365.2500598"},{"key":"13_CR42","unstructured":"Prawitz, D.: Natural Deduction: A proof-theoretical study. Stockholm Studies in Philosophy. Almqvist & Wiksell, Stockholm 3 (1965)"},{"key":"13_CR43","doi-asserted-by":"publisher","unstructured":"Radanne, G., Saffrich, H., Thiemann, P.: Kindly bent to free us. Proc. ACM Program. Lang. 4(ICFP) (Aug 2020). https:\/\/doi.org\/10.1145\/3408985","DOI":"10.1145\/3408985"},{"key":"13_CR44","doi-asserted-by":"crossref","unstructured":"Sammler, M., Lepigre, R., Krebbers, R., Memarian, K., Dreyer, D., Garg, D.: RefinedC: Automating the foundational verification of C code with refined ownership types. Proc. ACM Program. Lang. (Jun 2021)","DOI":"10.1145\/3453483.3454036"},{"key":"13_CR45","unstructured":"Scholz, S.B.: Single Assignment C - Entwurf und Implementierung einer funktionalen C-Variante mit spezieller Unterst\u00fctzung shape-invarianter Array-Operationen. Ph.D. thesis, Institut f\u00fcr Informatik und Praktische Mathematik, Christian-Albrechts-Universit\u00e4t, Kiel, Germany (1996), https:\/\/www.sac-home.org\/_media\/publications:pdf:sac-design-sbs-phd-96.pdf, Shaker Verlag, Aachen, 1997"},{"key":"13_CR46","doi-asserted-by":"publisher","unstructured":"Selinger, P., Valiron, B.: Quantum Lambda Calculus, p. 135\u2013172. Cambridge University Press (2009). https:\/\/doi.org\/10.1017\/CBO9781139193313.005","DOI":"10.1017\/CBO9781139193313.005"},{"key":"13_CR47","doi-asserted-by":"publisher","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. pp. 358\u2013379. Springer, Berlin Heidelberg, Berlin, Heidelberg (1994). https:\/\/doi.org\/10.1007\/3-540-57787-4_23","DOI":"10.1007\/3-540-57787-4_23"},{"key":"13_CR48","doi-asserted-by":"publisher","unstructured":"Somogyi, Z., Henderson, F., Conway, T.: The execution algorithm of Mercury, an efficient purely declarative logic programming language. The Journal of Logic Programming 29(1), 17\u201364 (1996). https:\/\/doi.org\/10.1016\/S0743-1066(96)00068-4, https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0743106696000684, high-Performance Implementations of Logic Programming Systems","DOI":"10.1016\/S0743-1066(96)00068-4"},{"key":"13_CR49","unstructured":"Spiwack, A., Kiss, C., Bernardy, J.P., Wu, N., Eisenberg, R.: Linear constraints (2021), https:\/\/arxiv.org\/abs\/2103.06127"},{"key":"13_CR50","doi-asserted-by":"crossref","unstructured":"Terui, K.: Light affine lambda calculus and polytime strong normalization. In: LICS \u201901. pp. 209\u2013220. IEEE Computer Society (2001)","DOI":"10.1109\/LICS.2001.932498"},{"key":"13_CR51","doi-asserted-by":"publisher","unstructured":"Tofte, M., Birkedal, L., Elsman, M., Hallenberg, N.: A Retrospective on Region-Based Memory Management. Higher-Order and Symbolic Computation 17(3), 245\u2013265 (Sep 2004). https:\/\/doi.org\/10.1023\/B:LISP.0000029446.78563.a4","DOI":"10.1023\/B:LISP.0000029446.78563.a4"},{"key":"13_CR52","doi-asserted-by":"publisher","unstructured":"Tov, J.A., Pucella, R.: Practical affine types. In: Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. p. 447\u2013458. POPL \u201911, Association for Computing Machinery, New York, NY, USA (2011). https:\/\/doi.org\/10.1145\/1926385.1926436","DOI":"10.1145\/1926385.1926436"},{"key":"13_CR53","doi-asserted-by":"publisher","unstructured":"de Vries, E.: Modelling unique and affine typing using polymorphism. In: Essays Dedicated to Rinus Plasmeijer on the Occasion of His 61st Birthday on The Beauty of Functional Code - Volume 8106. p. 181\u2013192. Springer-Verlag, Berlin, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40355-2_13","DOI":"10.1007\/978-3-642-40355-2_13"},{"key":"13_CR54","doi-asserted-by":"publisher","unstructured":"de Vries, E., Francalanza, A., Hennessy, M.: Uniqueness typing for resource management in message-passing concurrency. In: Florido, M., Mackie, I. (eds.) Proceedings First International Workshop on Linearity, LINEARITY 2009, Coimbra, Portugal, 12th September 2009. EPTCS, vol. 22, pp. 26\u201337 (2009). https:\/\/doi.org\/10.4204\/EPTCS.22.3","DOI":"10.4204\/EPTCS.22.3"},{"key":"13_CR55","doi-asserted-by":"crossref","unstructured":"de Vries, E., Plasmeijer, R., Abrahamson, D.M.: Uniqueness typing redefined. In: Proceedings of the 18th International Conference on Implementation and Application of Functional Languages. p. 181\u2013198. IFL\u201906, Springer-Verlag, Berlin, Heidelberg (2006)","DOI":"10.1007\/978-3-540-74130-5_11"},{"key":"13_CR56","doi-asserted-by":"crossref","unstructured":"de\u00a0Vries, E., Plasmeijer, R., Abrahamson, D.M.: Uniqueness typing simplified. In: Chitil, O., Horv\u00e1th, Z., Zs\u00f3k, V. (eds.) Implementation and Application of Functional Languages. pp. 201\u2013218. Springer Berlin Heidelberg, Berlin, Heidelberg (2008)","DOI":"10.1007\/978-3-540-85373-2_12"},{"key":"13_CR57","unstructured":"Wadler, P.: Linear Types Can Change the World! In: Broy, M., Jones, C.B. (eds.) Programming Concepts and Methods: Proceedings of the IFIP Working Group 2.2\/2.3 Working Conference on Programming Concepts and Methods, Sea of Galilee, Israel, 2\u20135 April, 1990. pp. 561\u2013581. North-Holland, Amsterdam (1990), https:\/\/homepages.inf.ed.ac.uk\/wadler\/topics\/linear-logic.html#linear-types"},{"key":"13_CR58","doi-asserted-by":"publisher","unstructured":"Wadler, P.: Is there a use for linear logic? In: Proceedings of the 1991 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation. p. 255\u2013273. PEPM \u201991, Association for Computing Machinery, New York, NY, USA (1991). https:\/\/doi.org\/10.1145\/115865.115894","DOI":"10.1145\/115865.115894"},{"key":"13_CR59","unstructured":"Wadler, P.: There\u2019s no substitute for linear logic. In: 8th International Workshop on the Mathematical Foundations of Programming Semantics (1992)"},{"key":"13_CR60","doi-asserted-by":"publisher","unstructured":"Wadler, P.: A syntax for linear logic. In: Mathematical Foundations of Programming Semantics, 9th International Conference, New Orleans, LA, USA, April 7\u201310, 1993, Proceedings. pp. 513\u2013529 (1993). https:\/\/doi.org\/10.1007\/3-540-58027-1_24","DOI":"10.1007\/3-540-58027-1_24"},{"key":"13_CR61","doi-asserted-by":"crossref","unstructured":"Wadler, P.: A taste of linear logic. In: Borzyszkowski, A.M., Soko\u0142owski, S. (eds.) Mathematical Foundations of Computer Science 1993. pp. 185\u2013210. Springer Berlin Heidelberg, Berlin, Heidelberg (1993)","DOI":"10.1007\/3-540-57182-5_12"},{"key":"13_CR62","doi-asserted-by":"crossref","unstructured":"Walker, D.: Substructural type systems. Advanced Topics in Types and Programming Languages pp. 3\u201344 (2005)","DOI":"10.7551\/mitpress\/1104.003.0003"},{"key":"13_CR63","doi-asserted-by":"publisher","unstructured":"Walker, D., Crary, K., Morrisett, G.: Typed memory management via static capabilities. ACM Trans. Program. Lang. Syst. 22(4), 701\u2013771 (jul 2000). https:\/\/doi.org\/10.1145\/363911.363923","DOI":"10.1145\/363911.363923"},{"key":"13_CR64","unstructured":"Weiss, A., Gierczak, O., Patterson, D., Ahmed, A.: Oxide: The essence of Rust (2021), https:\/\/arxiv.org\/abs\/1903.00982"},{"key":"13_CR65","doi-asserted-by":"crossref","unstructured":"Zhu, D., Xi, H.: Safe programming with pointers through stateful views. In: Hermenegildo, M.V., Cabeza, D. (eds.) Practical Aspects of Declarative Languages. pp. 83\u201397. Springer Berlin Heidelberg, Berlin, Heidelberg (2005)","DOI":"10.1007\/978-3-540-30557-6_8"}],"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-3-030-99336-8_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,15]],"date-time":"2024-11-15T05:08:03Z","timestamp":1731647283000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-99336-8_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783030993351","9783030993368"],"references-count":65,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-99336-8_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"29 March 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ESOP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Symposium on Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Munich","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 April 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 April 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2022\/esop","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"HotCRP","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"64","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"21","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"33% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.5","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"7","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}