{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,18]],"date-time":"2026-08-18T14:14:04Z","timestamp":1787062444845,"version":"build-2736575974"},"reference-count":60,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2019,7,26]],"date-time":"2019-07-26T00:00:00Z","timestamp":1564099200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/M026124\/1"],"award-info":[{"award-number":["EP\/M026124\/1"]}],"id":[{"id":"10.13039\/501100000266","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":[[2019,7,26]]},"abstract":"<jats:p>In programming, some data acts as a resource (e.g., file handles, channels) subject to usage constraints. This poses a challenge to software correctness as most languages are agnostic to constraints on data. The approach of linear types provides a partial remedy, delineating data into resources to be used but never copied or discarded, and unconstrained values. Bounded Linear Logic provides a more fine-grained approach, quantifying non-linear use via an indexed-family of modalities. Recent work on coeffect types generalises this idea to graded comonads, providing type systems which can capture various program properties. Here, we propose the umbrella notion of graded modal types, encompassing coeffect types and dual notions of type-based effect reasoning via graded monads. In combination with linear and indexed types, we show that graded modal types provide an expressive type theory for quantitative program reasoning, advancing the reach of type systems to capture and verify a broader set of program properties. We demonstrate this approach via a type system embodied in a fully-fledged functional language called Granule, exploring various examples.<\/jats:p>","DOI":"10.1145\/3341714","type":"journal-article","created":{"date-parts":[[2019,7,29]],"date-time":"2019-07-29T16:55:51Z","timestamp":1564419351000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":63,"title":["Quantitative program reasoning with graded modal types"],"prefix":"10.1145","volume":"3","author":[{"given":"Dominic","family":"Orchard","sequence":"first","affiliation":[{"name":"University of Kent, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Vilem-Benjamin","family":"Liepelt","sequence":"additional","affiliation":[{"name":"University of Kent, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Harley","family":"Eades III","sequence":"additional","affiliation":[{"name":"Augusta University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,7,26]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(93)90181-R"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951948"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209189"},{"key":"e_1_2_2_4_1","volume-title":"Context Constrained Computation. In Workshop on Type-Driven Development, colocated with ICFP","author":"Atkey Robert","year":"2018"},{"key":"e_1_2_2_5_1","volume-title":"Dual intuitionistic linear logic","author":"Barber Andrew"},{"key":"e_1_2_2_6_1","volume-title":"Proceedings of the 8th International Workshop on Satisfiability Modulo Theories","volume":"13","author":"Barrett Clark","year":"2010"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796898002998"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158093"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1005291931660"},{"key":"e_1_2_2_10_1","volume-title":"24th EACSL Annual Conference on Computer Science Logic (CSL","author":"Breuvart Flavien","year":"2015"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_19"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/36583.36603"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/1887654.1887670"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2001.2951"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2011.22"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328897.1328457"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2746325.2746335"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009890"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2544174.2500582"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290322"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964025"},{"key":"e_1_2_2_23_1","volume-title":"Towards a formal theory of graded monads","author":"Fujii Soichiro"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429113"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951939"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796809990268"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_18"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90386-T"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111542.1111550"},{"key":"e_1_2_2_32_1","volume-title":"Haskell 98 language and libraries: the revised report","author":"Jones Simon Peyton"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535846"},{"key":"e_1_2_2_34_1","volume-title":"International Conference on Foundations of Software Science and Computation Structures. Springer, 110\u2013127","year":"2018"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676969"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2692956.2663188"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1708016.1708027"},{"key":"e_1_2_2_38_1","volume-title":"Nuttin\u2019. In A List of Successes That Can Change the World","author":"McBride Conor"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796803004829"},{"key":"e_1_2_2_40_1","volume-title":"6th Conference on Algebra and Coalgebra in Computer Science (CALCO","author":"Milius Stefan","year":"2015"},{"key":"e_1_2_2_41_1","doi-asserted-by":"crossref","volume-title":"The Definition of Standard ML: revised","author":"Milner Robin","DOI":"10.7551\/mitpress\/2319.001.0001"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951925"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-27810-0_1"},{"key":"e_1_2_2_44_1","volume-title":"Workshop on Trends in Linear Logic and Applications (TLLA).","author":"Orchard Dominic","year":"2017"},{"key":"e_1_2_2_45_1","volume-title":"The semantic marriage of monads and effects. CoRR abs\/1401.5391","author":"Orchard Dominic A.","year":"2014"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39212-2_35"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628160"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/1160074.1159811"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129501003322"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/2804302.2804309"},{"key":"e_1_2_2_51_1","volume-title":"Natural Deduction: A proof-theoretical study.","author":"Prawitz Dag","year":"1965"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10958-008-9013-7"},{"key":"e_1_2_2_53_1","volume-title":"LICS \u201901","author":"Terui K."},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11957-6_29"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926436"},{"key":"e_1_2_2_56_1","first-page":"347","article-title":"Linear types can change the world","volume":"2","author":"Wadler Philip","year":"1990","journal-title":"IFIP TC"},{"key":"e_1_2_2_57_1","volume-title":"8th International Workshop on the Mathematical Foundations of Programming Semantics.","author":"Wadler Philip","year":"1992"},{"key":"e_1_2_2_58_1","volume-title":"9th International Conference","author":"Wadler Philip","year":"1993"},{"key":"e_1_2_2_59_1","volume-title":"Substructural type systems. Advanced Topics in Types and Programming Languages","author":"Walker David","year":"2005"},{"key":"e_1_2_2_60_1","volume-title":"International Workshop on Types for Proofs and Programs. Springer, 394\u2013408","author":"Xi Hongwei","year":"2003"},{"key":"e_1_2_2_61_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.02.056"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3341714","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3341714","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:43:24Z","timestamp":1750193004000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3341714"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,7,26]]},"references-count":60,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2019,7,26]]}},"alternative-id":["10.1145\/3341714"],"URL":"https:\/\/doi.org\/10.1145\/3341714","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,7,26]]},"assertion":[{"value":"2019-07-26","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}