{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,26]],"date-time":"2026-09-26T08:58:41Z","timestamp":1790413121072,"version":"4.1.0"},"reference-count":52,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2026,8,17]],"date-time":"2026-08-17T00:00:00Z","timestamp":1786924800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"funder":[{"name":"EPSRC","award":["EP\/T013516\/1"],"award-info":[{"award-number":["EP\/T013516\/1"]}],"id":[{"id":"https:\/\/ror.org\/0439y7842","id-type":"ROR","asserted-by":"crossref"}]},{"name":"Schmidt Sciences, LLC","award":["-"],"award-info":[{"award-number":["-"]}],"id":[{"id":"https:\/\/ror.org\/044fk6795","id-type":"ROR","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2026,8,17]]},"abstract":"<jats:p>\n                    <jats:italic toggle=\"yes\">Graded types<\/jats:italic>\n                    provide a way to augment a type system with fine-grained information, e.g., to track side effects or context dependence and resource use (called\n                    <jats:italic toggle=\"yes\">coeffects<\/jats:italic>\n                    ). Graded types for coeffects have found their way into languages such as Haskell, Idris, and Granule, enabling resourceful reasoning via coeffect analysis with varying levels of generality. Two separate lineages of graded coeffect system have emerged in the last decade: those in which coeffect annotations are pervasive, requiring annotations on function types (which we call\n                    <jats:italic toggle=\"yes\">graded-base<\/jats:italic>\n                    ) and those in which coeffects are added by way of a graded modal type operator atop linear types (which we call\n                    <jats:italic toggle=\"yes\">linear-base<\/jats:italic>\n                    ). The latter has its origins in Girard\u2019s Linear Logic which has been a rich humus for programming language research focused on resources, whereas the graded-base approach emerged in the mid-2010s, seeing rapid adoption in programming language theory and practice, e.g. in QTT and Linear Haskell. The relationship between these two styles has however remained an open question. We answer this question by giving translations between pairs of calculi of both lineages that we prove type-, grade- and operational-semantics preserving. We show that the same notions of context dependence can be expressed in either style, building a bridge between the two lineages that enables transfer of results and ideas, while helping language designers to make better informed choices.\n                  <\/jats:p>","DOI":"10.1145\/3828697","type":"journal-article","created":{"date-parts":[[2026,8,17]],"date-time":"2026-08-17T20:23:46Z","timestamp":1786998226000},"page":"721-750","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Same Coeffect, Different Base: Connecting Two Dominant Approaches to Graded Types"],"prefix":"10.1145","volume":"10","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2198-1819","authenticated-orcid":false,"given":"Vilem","family":"Liepelt","sequence":"first","affiliation":[{"name":"University of Kent, Canterbury, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4284-3757","authenticated-orcid":false,"given":"Danielle","family":"Marshall","sequence":"additional","affiliation":[{"name":"Royal Holloway, University of London, London, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7058-7842","authenticated-orcid":false,"given":"Dominic","family":"Orchard","sequence":"additional","affiliation":[{"name":"University of Cambridge, Cambridge, United Kingdom"},{"name":"University of Kent, Canterbury, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,8,17]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408972"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3607862"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","unstructured":"Robert Atkey. 2018. Syntax and Semantics of Quantitative Type Theory. In Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science LICS 2018 Oxford UK July 09-12 2018. 56\u201365. doi:10.1145\/3209108.3209189","DOI":"10.1145\/3209108.3209189"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFB0022251"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158093"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ECOOP.2023.3"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3622843"},{"key":"e_1_3_1_9_1","article-title":"Don\u2019t exhaust, don\u2019t waste","author":"Bianchini Riccardo","year":"2025","unstructured":"Riccardo Bianchini, Francesco Dagnino, Paola Giannini, and Elena Zucca. 2025. Don\u2019t exhaust, don\u2019t waste. CoRR abs\/2507.13792 (2025). arXiv:2507.13792 doi:10.48550\/ARXIV.2507.13792","journal-title":"CoRR"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563319"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ECOOP.2021.9"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.4230\/DARTS.7.2.10"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_19"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434331"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49630-5_30"},{"key":"e_1_3_1_16_1","doi-asserted-by":"crossref","unstructured":"Marco Gaboardi Andreas Haeberlen Justin Hsu Arjun Narayan and Benjamin C Pierce. 2013. Linear dependent types for differential privacy. In Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages. 357\u2013370.","DOI":"10.1145\/2429069.2429113"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951939"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3704859"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_18"},{"key":"e_1_3_1_20_1","doi-asserted-by":"crossref","unstructured":"David K Gifford and John M Lucassen. 1986. Integrating functional and imperative programming. In Proceedings of the 1986 ACM Conference on LISP and Functional Programming. 28\u201338.","DOI":"10.1145\/319838.319848"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90386-T"},{"key":"e_1_3_1_23_1","unstructured":"Jack Hughes Danielle Marshall James Wood and Dominic Orchard. 2021. 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":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-68446-4_8"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-57262-3_4"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","unstructured":"Jack Hughes Michael Vollmer and Dominic Orchard. 2020. Deriving Distributive Laws for Graded Linear Types. In Proceedings Second Joint International Workshop on Linearity & Trends in Linear Logic and Applications Linearity&TLLA@IJCAR-FSCD 2020 Online 29-30 June 2020 (EPTCS Vol. 353) Ugo Dal Lago and Valeria de Paiva (Eds.). 109\u2013131. doi:10.4204\/EPTCS.353.6","DOI":"10.4204\/EPTCS.353.6"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535846"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2606.28042"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-032-08187-2_7"},{"key":"e_1_3_1_30_1","doi-asserted-by":"crossref","unstructured":"Sam Lindley. 2025. Encoding Product Types. In Proceedings of the Workshop Dedicated to Olivier Danvy on the Occasion of His 64th Birthday. 142\u2013151.","DOI":"10.1145\/3759427.3760375"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3674642"},{"key":"e_1_3_1_32_1","doi-asserted-by":"crossref","unstructured":"John M Lucassen and David K Gifford. 1988. Polymorphic effect systems. In Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. 47\u201357.","DOI":"10.1145\/73560.73564"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-30936-1_12"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1989.39155"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"e_1_3_1_36_1","doi-asserted-by":"crossref","unstructured":"B Moon H Eades III and D Orchard. 2021. Graded Modal Dependent Type Theory. In Programming Languages and Systems30th European Symposium on Programming ESOP 2021 Held as Part of the European Joint Conferences on Theory and Practice of Software ETAPS 2021 Luxembourg City Luxembourg March 27\u2013April 1 2021 Proceedings Vol. 12648. 462\u2013490.","DOI":"10.1007\/978-3-030-72019-3_17"},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-27810-0_1"},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-03811-6_5"},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341714"},{"key":"e_1_3_1_40_1","unstructured":"Dominic A. Orchard Tomas Petricek and Alan Mycroft. 2014. The semantic marriage of monads and effects. CoRR abs\/1401.5391 (2014). arXiv:1401.5391 http:\/\/arxiv.org\/abs\/1401.5391"},{"key":"e_1_3_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628160"},{"key":"e_1_3_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39212-2_35"},{"key":"e_1_3_1_43_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(75)90017-1"},{"key":"e_1_3_1_44_1","unstructured":"The GHC Developers. 2020. GHC User\u2019s Guide:Linear Types. https:\/\/web.archive.org\/web\/20241206233933\/https:\/\/downloads.haskell.org\/ghc\/9.0.1\/docs\/html\/users_guide\/exts\/linear_types.html"},{"key":"e_1_3_1_45_1","article-title":"Effects and Coeffects in Call-By-Push-Value (Extended Version)","author":"Torczon Cassia","year":"2023","unstructured":"Cassia Torczon, Emmanuel Su\u00e1rez Acevedo, Shubh Agrawal, Joey Velez-Ginorio, and Stephanie Weirich. 2023. Effects and Coeffects in Call-By-Push-Value (Extended Version). CoRR abs\/2311.11795 (2023). arXiv:2311.11795 doi:10.48550\/ARXIV. 2311.11795","journal-title":"CoRR"},{"key":"e_1_3_1_46_1","article-title":"Liquid Haskell as a GHC Plugin. Presented at the Haskell Implementors\u2019","author":"Vazou Niki","year":"2020","unstructured":"Niki Vazou, Eric Seidel, Richard Eisenberg, Simon Peyton Jones, and Dimitrios Vytiniotis. 2020. Liquid Haskell as a GHC Plugin. Presented at the Haskell Implementors\u2019 Workshop (HIW) 2020. https:\/\/icfp20.sigplan.org\/details\/hiw-2020-papers\/1\/Liquid-Haskell-as-a-GHC-Plugin","journal-title":"Workshop (HIW) 2020"},{"key":"e_1_3_1_47_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.CSL.2025.32"},{"key":"e_1_3_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/601775.601776"},{"key":"e_1_3_1_49_1","first-page":"3","article-title":"Substructural type systems","author":"Walker David","year":"2005","unstructured":"David Walker. 2005. Substructural type systems. Advanced topics in types and programming languages (2005), 3\u201344.","journal-title":"Advanced topics in types and programming languages"},{"key":"e_1_3_1_50_1","article-title":"A linear algebra approach to linear metatheory","author":"Wood James","year":"2020","unstructured":"James Wood and Robert Atkey. 2020. A linear algebra approach to linear metatheory. arXiv preprint arXiv:2005.02247 (2020).","journal-title":"arXiv preprint arXiv:2005.02247"},{"key":"e_1_3_1_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99336-8_14"},{"key":"e_1_3_1_52_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.20739966"},{"key":"e_1_3_1_53_1","doi-asserted-by":"publisher","DOI":"10.5555\/647164.717818"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3828697","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,9,26]],"date-time":"2026-09-26T08:10:16Z","timestamp":1790410216000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3828697"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,8,17]]},"references-count":52,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2026,8,17]]}},"alternative-id":["10.1145\/3828697"],"URL":"https:\/\/doi.org\/10.1145\/3828697","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,8,17]]},"assertion":[{"value":"2026-02-19","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-05-13","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-08-17","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}