{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T01:48:30Z","timestamp":1784166510829,"version":"3.55.0"},"reference-count":30,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2021,1,4]],"date-time":"2021-01-04T00:00:00Z","timestamp":1609718400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"NSF","award":["1521539"],"award-info":[{"award-number":["1521539"]}]},{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["1704041"],"award-info":[{"award-number":["1704041"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2021,1,4]]},"abstract":"<jats:p>Graded Type Theory provides a mechanism to track and reason about resource usage in type systems. In this paper, we develop GraD, a novel version of such a graded dependent type system that includes functions, tensor products, additive sums, and a unit type. Since standard operational semantics is resource-agnostic, we develop a heap-based operational semantics and prove a soundness theorem that shows correct accounting of resource usage. Several useful properties, including the standard type soundness theorem, non-interference of irrelevant resources in computation and single pointer property for linear resources, can be derived from this theorem. We hope that our work will provide a base for integrating linearity, irrelevance and dependent types in practical programming languages like Haskell.<\/jats:p>","DOI":"10.1145\/3434331","type":"journal-article","created":{"date-parts":[[2021,1,4]],"date-time":"2021-01-04T12:34:24Z","timestamp":1609763664000},"page":"1-32","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":28,"title":["A graded dependent type system with a usage-aware semantics"],"prefix":"10.1145","volume":"5","author":[{"given":"Pritam","family":"Choudhury","sequence":"first","affiliation":[{"name":"University of Pennsylvania, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Harley","family":"Eades III","sequence":"additional","affiliation":[{"name":"Augusta University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Richard A.","family":"Eisenberg","sequence":"additional","affiliation":[{"name":"Tweag I\/O, France \/ Bryn Mawr College, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Stephanie","family":"Weirich","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2021,1,4]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292555"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408972"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","unstructured":"Andreas Abel and Gabriel Scherer. 2012. On Irrelevance and Algorithmic Equality in Predicative Type Theory. Logical Methods in Computer Science 8 1 ( 2012 ). https:\/\/doi.org\/10.2168\/LMCS-8( 1 :29) 2012 10.2168\/LMCS-8(1:29)2012","DOI":"10.2168\/LMCS-8("},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209189"},{"key":"e_1_2_1_5_1","volume-title":"Foundations of Software Science and Computational Structures (FOSSACS 2008 )","author":"Barras Bruno","unstructured":"Bruno Barras and Bruno Bernardo. 2008. The Implicit Calculus of Constructions as a Programming Language with Dependent Types. In Foundations of Software Science and Computational Structures (FOSSACS 2008 ), Roberto Amadio (Ed.). Springer Berlin Heidelberg, Budapest, Hungary, 365-379."},{"key":"e_1_2_1_6_1","volume-title":"Selected Papers from the 8th International Workshop on Computer Science Logic (CSL '94)","author":"Benton P. N.","unstructured":"P. N. Benton. 1995. A Mixed Linear and Non-Linear Logic: Proofs, Terms and Models (Extended Abstract). In Selected Papers from the 8th International Workshop on Computer Science Logic (CSL '94). Springer-Verlag, London, UK, UK, 121-135."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158093"},{"key":"e_1_2_1_8_1","unstructured":"Guillaume Bonfante Fran\u00e7ois Lamarche and Thomas Streicher. 2001. A model of a dependent linear calculus. Intern report A01-R-262 || bonfante01c."},{"key":"e_1_2_1_9_1","unstructured":"Edwin Brady. 2020. Idris 2: Quantitative Type Theory in Action. (Feb. 2020 ). Draft available from https:\/\/www.typedriven.org.uk\/edwinb\/idris-2-quantitative-type-theory-in-action.html."},{"key":"e_1_2_1_10_1","volume-title":"A Core Quantitative Coefect Calculus","author":"Brunel Alo\u00efs","unstructured":"Alo\u00efs Brunel, Marco Gaboardi, Damiano Mazza, and Steve Zdancewic. 2014. A Core Quantitative Coefect Calculus. In Programming Languages and Systems, Zhong Shao (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 351-370."},{"key":"e_1_2_1_11_1","doi-asserted-by":"crossref","unstructured":"Iliano Cervesato and Frank Pfenning. 2002. A Linear Logical Framework. Information and Computation 179 1 ( 2002 ) 19-75.","DOI":"10.1006\/inco.2001.2951"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800001660"},{"key":"e_1_2_1_13_1","volume-title":"Revisited","author":"Lago Ugo Dal","unstructured":"Ugo Dal Lago and Martin Hofmann. 2009. Bounded Linear Logic, Revisited. In Typed Lambda Calculi and Applications, Pierre-Louis Curien (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 80-94."},{"key":"e_1_2_1_14_1","first-page":"115","volume-title":"Proceedings of the 14th Symposium on Principles and Practice of Declarative Programming (PPDP '12)","author":"Ugo","unstructured":"Ugo Dal lago and Barbara Petit. 2012. Linear Dependent Types in a Call-by-Value Scenario. In Proceedings of the 14th Symposium on Principles and Practice of Declarative Programming (PPDP '12). Association for Computing Machinery, New York, NY, USA, 115-126."},{"key":"e_1_2_1_15_1","unstructured":"Richard A. Eisenberg. 2016. Dependent Types in Haskell: Theory and Practice. Ph.D. Dissertation. University of Pennsylvania."},{"key":"e_1_2_1_16_1","unstructured":"Richard A. Eisenberg. 2018. Quantifiers for Dependent Haskell. GHC Proposal # 102. https:\/\/github.com\/goldfirere\/ghcproposals\/blob\/pi\/proposals\/0000-pi.rst"},{"key":"e_1_2_1_17_1","first-page":"357","volume-title":"Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '13)","author":"Gaboardi Marco","unstructured":"Marco Gaboardi, Andreas Haeberlen, Justin Hsu, Arjun Narayan, and Benjamin C. Pierce. 2013. Linear Dependent Types for Diferential Privacy. In Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '13). Association for Computing Machinery, New York, NY, USA, 357-370."},{"key":"e_1_2_1_18_1","first-page":"476","article-title":"Combining efects and coefects via grading","author":"Gaboardi Marco","year":"2016","unstructured":"Marco Gaboardi, Shin-ya Katsumata, Dominic A Orchard, Flavien Breuvart, and Tarmo Uustalu. 2016. Combining efects and coefects via grading. In ICFP. 476-489.","journal-title":"ICFP."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_18"},{"key":"e_1_2_1_20_1","volume-title":"Scott","author":"Girard Jean-Yves","year":"1992","unstructured":"Jean-Yves Girard, Andre Scedrov, and Philip J. Scott. 1992. Bounded linear logic: a modular approach to polynomial-time computability. Theoretical Computer Science 97, 1 ( 1992 ), 1-66."},{"key":"e_1_2_1_21_1","volume-title":"Semirings and their Applications","author":"Golan Jonathan S.","year":"2013","unstructured":"Jonathan S. Golan. 1999. Semirings and their Applications. Springer Netherlands. https:\/\/doi.org\/10.1007\/ 978-94-015-9333-5 Adam Gundry. 2013. Type Inference, Haskell and Dependent Types. Ph.D. Dissertation. University of Strathclyde."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676969"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/158511.158618"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45413-6_27"},{"key":"e_1_2_1_25_1","volume-title":"Harley Eades III, and Dominic Orchard","author":"Moon Benjamin","year":"2020","unstructured":"Benjamin Moon, Harley Eades III, and Dominic Orchard. 2020. Graded Modal Dependent Type Theory (Extended Abstract). TyDe (May 2020 )."},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863568"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.5555\/353629.353648"},{"key":"e_1_2_1_28_1","first-page":"347","article-title":"Linear types can change the world","volume":"2","author":"Wadler Philip","year":"1990","unstructured":"Philip Wadler. 1990. Linear types can change the world. In IFIP TC, Vol. 2. 347-359.","journal-title":"IFIP TC"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341705"},{"key":"e_1_2_1_30_1","volume-title":"A Linear Algebra Approach to Linear Metatheory. arXiv","author":"Wood James","year":"2005","unstructured":"James Wood and Robert Atkey. 2020. A Linear Algebra Approach to Linear Metatheory. arXiv: 2005. 02247 [cs.PL]"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3434331","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3434331","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3434331","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T07:27:12Z","timestamp":1781854032000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3434331"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,1,4]]},"references-count":30,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2021,1,4]]}},"alternative-id":["10.1145\/3434331"],"URL":"https:\/\/doi.org\/10.1145\/3434331","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,1,4]]},"assertion":[{"value":"2021-01-04","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}