@article(abel-barnardy-icfp2020,
 author       = {Andreas Abel and Jean-Philippe Bernardy},
 year         = {2020},
 title        = {A Unified View of Modalities in Type Systems},
 journal      = {Proc. ACM Program. Lang.},
 volume       = {4},
 number       = {ICFP},
 doi          = {10.1145/3408972},
)
@inproceedings(benton1992linear,
 author       = {Nick Benton and Gavin Bierman and De Paiva, Valeria and Martin Hyland},
 year         = {1992},
 title        = {Linear lambda-calculus and categorical models revisited},
 booktitle    = {International Workshop on Computer Science Logic},
 organization = {Springer},
 pages        = {61--84},
 doi          = {10.1007/3-540-56992-8\_6},
)
@article(linear-haskell,
 author       = {Jean-Philippe Bernardy and Mathieu Boespflug and Ryan R. Newton and Peyton Jones, Simon and Arnaud Spiwack},
 year         = {2017},
 title        = {Linear {H}askell: Practical Linearity in a Higher-Order Polymorphic Language},
 journal      = {Proc. ACM Program. Lang.},
 volume       = {2},
 number       = {POPL},
 doi          = {10.1145/3158093},
)
@inproceedings(bradyidris,
 author       = {Edwin Brady},
 year         = {2021},
 title        = {{Idris 2: Quantitative Type Theory in Practice}},
 editor       = {M{\o}ller, Anders and Manu Sridharan},
 booktitle    = {35th European Conference on Object-Oriented Programming (ECOOP 2021)},
 series       = {Leibniz International Proceedings in Informatics (LIPIcs)},
 volume       = {194},
 publisher    = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
 address      = {Dagstuhl, Germany},
 pages        = {9:1--9:26},
 doi          = {10.4230/LIPIcs.ECOOP.2021.9},
 url          = {https://drops.dagstuhl.de/opus/volltexte/2021/14052},
)
@techreport(brookes1993intensional,
 author       = {Stephen Brookes and Kathryn V Stone},
 year         = {1993},
 title        = {Monads and Comonads in Intensional Semantics},
 type         = {Technical Report},
 address      = {Pittsburgh, PA, USA},
 url          = {https://dl.acm.org/doi/10.5555/865105},
)
@inproceedings(brunel2014core,
 author       = {Alo{\"\i}s Brunel and Marco Gaboardi and Damiano Mazza and Steve Zdancewic},
 year         = {2014},
 title        = {A core quantitative coeffect calculus},
 booktitle    = {European Symposium on Programming Languages and Systems},
 organization = {Springer},
 pages        = {351--370},
 doi          = {10.1007/978-3-642-54833-8\_19},
)
@article(choudhury2021,
 author       = {Pritam Choudhury and Eades III, Harley and Richard A. Eisenberg and Stephanie Weirich},
 year         = {2021},
 title        = {A Graded Dependent Type System with a Usage-Aware Semantics},
 journal      = {Proc. ACM Program. Lang.},
 volume       = {5},
 number       = {POPL},
 doi          = {10.1145/3434331},
)
@inproceedings(eisenberg2016visible,
 author       = {Richard A Eisenberg and Stephanie Weirich and Hamidhasan G Ahmed},
 year         = {2016},
 title        = {Visible type application},
 booktitle    = {European Symposium on Programming},
 organization = {Springer},
 pages        = {229--254},
 doi          = {10.1007/978-3-662-49498-1\_10},
)
@inproceedings(gaboardi2013linear,
 author       = {Marco Gaboardi and Andreas Haeberlen and Justin Hsu and Arjun Narayan and Benjamin C Pierce},
 year         = {2013},
 title        = {Linear dependent types for differential privacy},
 booktitle    = {Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
 pages        = {357--370},
 doi          = {10.1145/2429069.2429113},
)
@inproceedings(combining2016,
 author       = {Marco Gaboardi and Shin-ya Katsumata and Dominic Orchard and Flavien Breuvart and Tarmo Uustalu},
 year         = {2016},
 title        = {Combining {E}ffects and {C}oeffects via {G}rading},
 booktitle    = {Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming},
 series       = {ICFP 2016},
 publisher    = {Association for Computing Machinery},
 address      = {New York, NY, USA},
 pages        = {476\IeC{\textendash}489},
 doi          = {10.1145/2951913.2951939},
)
@incollection(ghica2014bounded,
 author       = {Dan R. Ghica and Alex I. Smith},
 year         = {2014},
 title        = {Bounded linear types in a resource semiring},
 booktitle    = {Programming Languages and Systems},
 publisher    = {Springer},
 pages        = {331--350},
 doi          = {10.1007/978-3-642-54833-8\_18},
)
@article(girard1987linear,
 author       = {Jean-Yves Girard},
 year         = {1987},
 title        = {Linear logic},
 journal      = {Theoretical computer science},
 volume       = {50},
 number       = {1},
 pages        = {1--101},
 doi          = {10.1016/0304-3975(87)90045-4},
)
@article(girard1992bounded,
 author       = {Jean-Yves Girard and Andre Scedrov and Philip J Scott},
 year         = {1992},
 title        = {Bounded linear logic: a modular approach to polynomial-time computability},
 journal      = {Theoretical computer science},
 volume       = {97},
 number       = {1},
 pages        = {1--66},
 doi          = {10.1016/0304-3975(92)90386-T},
)
@inproceedings(hinze2000new,
 author       = {Ralf Hinze},
 year         = {2000},
 title        = {A new approach to generic functional programming},
 booktitle    = {Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
 pages        = {119--132},
 doi          = {10.1145/325694.325709},
)
@inproceedings(hughes:lirmm-03271465,
 author       = {Jack Hughes and Daniel Marshall and James Wood and Dominic Orchard},
 year         = {2021},
 title        = {{Linear Exponentials as Graded Modal Types}},
 booktitle    = {{5th International Workshop on Trends in Linear Logic and Applications (TLLA 2021)}},
 address      = {Rome (virtual), Italy},
 url          = {https://hal-lirmm.ccsd.cnrs.fr/lirmm-03271465},
)
@inproceedings(DBLP:conf/lopstr/HughesO20,
 author       = {Jack Hughes and Dominic Orchard},
 year         = {2020},
 title        = {Resourceful Program Synthesis from Graded Linear Types},
 booktitle    = {Logic-Based Program Synthesis and Transformation - 30th International Symposium, {LOPSTR} 2020, Bologna, Italy, September 7-9, 2020, Proceedings},
 pages        = {151--170},
 doi          = {10.1007/978-3-030-68446-4\_8},
)
@misc(appendix,
 author       = {Jack Hughes and Michael Vollmer and Dominic Orchard},
 year         = {2021},
 title        = {{Deriving Distributive Laws for Graded Linear Types (Additional Material)}},
 doi          = {10.5281/zenodo.5575771},
 url          = {https://doi.org/10.5281/zenodo.5575771},
)
@inproceedings(jay1994shapely,
 author       = {C Barry Jay and J Robin B Cockett},
 year         = {1994},
 title        = {Shapely types and shape polymorphism},
 booktitle    = {European Symposium on Programming},
 organization = {Springer},
 pages        = {302--316},
 doi          = {10.1007/3-540-57880-3\_20},
)
@inproceedings(DBLP:conf/popl/Katsumata14,
 author       = {Shin{-}ya Katsumata},
 year         = {2014},
 title        = {Parametric effect monads and semantics of effect systems},
 editor       = {Suresh Jagannathan and Peter Sewell},
 booktitle    = {The 41st Annual {ACM} {SIGPLAN-SIGACT} Symposium on Principles of Programming Languages, {POPL} '14, San Diego, CA, USA, January 20-21, 2014},
 publisher    = {{ACM}},
 pages        = {633--646},
 doi          = {10.1145/2535838.2535846},
)
@inproceedings(DBLP:conf/fossacs/Katsumata18,
 author       = {Shin{-}ya Katsumata},
 year         = {2018},
 title        = {A Double Category Theoretic Analysis of Graded Linear Exponential Comonads},
 editor       = {Christel Baier and Ugo Dal Lago},
 booktitle    = {Foundations of Software Science and Computation Structures - 21st International Conference, {FOSSACS} 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {10803},
 publisher    = {Springer},
 pages        = {110--127},
 doi          = {10.1007/978-3-319-89366-2\_6},
)
@article(generic-deriving,
 author       = {Magalh\~{a}es, Jos\'{e} Pedro and Atze Dijkstra and Johan Jeuring and Andres L\"{o}h},
 year         = {2010},
 title        = {A {G}eneric {D}eriving {M}echanism for {H}askell},
 journal      = {SIGPLAN Not.},
 volume       = {45},
 number       = {11},
 pages        = {37\IeC{\textendash}48},
 doi          = {10.1145/2088456.1863529},
)
@article(DBLP:journals/pacmpl/OrchardLE19,
 author       = {Dominic Orchard and Vilem{-}Benjamin Liepelt and Harley Eades III},
 year         = {2019},
 title        = {Quantitative program reasoning with graded modal types},
 journal      = {{PACMPL}},
 volume       = {3},
 number       = {{ICFP}},
 pages        = {110:1--110:30},
 doi          = {10.1145/3341714},
)
@inproceedings(petricek2014coeffects,
 author       = {Tomas Petricek and Dominic Orchard and Alan Mycroft},
 year         = {2014},
 title        = {Coeffects: a calculus of context-dependent computation},
 booktitle    = {Proceedings of the 19th ACM SIGPLAN international conference on Functional programming},
 organization = {ACM},
 pages        = {123--135},
 doi          = {10.1145/2692915.2628160},
)
@inproceedings(DBLP:conf/icalp/PetricekOM13,
 author       = {Tomas Petricek and Dominic A. Orchard and Alan Mycroft},
 year         = {2013},
 title        = {Coeffects: Unified Static Analysis of Context-Dependence},
 editor       = {Fedor V. Fomin and Rusins Freivalds and Marta Z. Kwiatkowska and David Peleg},
 booktitle    = {Automata, Languages, and Programming - 40th International Colloquium, {ICALP} 2013, Riga, Latvia, July 8-12, 2013, Proceedings, Part {II}},
 series       = {Lecture Notes in Computer Science},
 volume       = {7966},
 publisher    = {Springer},
 pages        = {385--397},
 doi          = {10.1007/978-3-642-39212-2\_35},
)
@article(power2002combining,
 author       = {John Power and Hiroshi Watanabe},
 year         = {2002},
 title        = {Combining a monad and a comonad},
 journal      = {Theoretical Computer Science},
 volume       = {280},
 number       = {1-2},
 pages        = {137--162},
 doi          = {10.1016/S0304-3975(01)00024-X},
)
@inproceedings(template-haskell,
 author       = {Tim Sheard and Simon Peyton Jones},
 year         = {2002},
 title        = {Template Meta-Programming for {H}askell},
 booktitle    = {Proceedings of the 2002 ACM SIGPLAN Workshop on Haskell},
 series       = {Haskell '02},
 publisher    = {Association for Computing Machinery},
 address      = {New York, NY, USA},
 pages        = {1\IeC{\textendash}16},
 doi          = {10.1145/581690.581691},
)
@article(street1972formal,
 author       = {Ross Street},
 year         = {1972},
 title        = {The formal theory of monads},
 journal      = {Journal of Pure and Applied Algebra},
 volume       = {2},
 number       = {2},
 pages        = {149--168},
 doi          = {10.1016/0022-4049(72)90019-9},
)
@inproceedings(Terui01lics,
 author       = {K. Terui},
 year         = {2001},
 title        = {Light Affine Lambda Calculus and Polytime Strong Normalization},
 booktitle    = {\rm {LICS '01}},
 publisher    = {IEEE Computer Society},
 pages        = {209--220},
 doi          = {10.1109/LICS.2001.932498},
)
@article(uustalu2006essence,
 author       = {Tarmo Uustalu and Varmo Vene},
 year         = {November 2006},
 title        = {The {E}ssence of {D}ataflow {P}rogramming},
 journal      = {Lecture Notes in Computer Science},
 volume       = {4164},
 pages        = {135--167},
 doi          = {10.1007/11894100\_5},
)