@article(AACMM20,
 author       = {Guillaume Allais and Robert Atkey and James Chapman and Conor McBride and James McKinna},
 year         = {2021},
 title        = {A type- and scope-safe universe of syntaxes with binding: their semantics and proofs},
 journal      = {Journal of Functional Programming},
 volume       = {31},
 pages        = {e22},
 doi          = {10.1017/S0956796820000076},
)
@article(AbelBernardy2020,
 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(allais:LIPIcs:2018:10049,
 author       = {Guillaume Allais},
 year         = {2018},
 title        = {{Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic}},
 booktitle    = {TYPES 2017},
 pages        = {1:1--1:22},
 doi          = {10.4230/LIPIcs.TYPES.2017.1},
)
@techreport(Barber1996,
 author       = {Andrew Barber},
 year         = {1996},
 title        = {Dual Intuitionistic Linear Logic},
 type         = {Technical Report},
 institution  = {University of Edinburgh},
)
@inproceedings(BentonBPH93,
 author       = {P. N. Benton and Gavin M. Bierman and Valeria de Paiva and Martin Hyland},
 year         = {1993},
 title        = {A Term Calculus for Intuitionistic Linear Logic},
 booktitle    = {Typed Lambda Calculi and Applications},
 series       = {LNCS},
 volume       = {664},
 publisher    = {Springer},
 pages        = {75--90},
 doi          = {10.1007/BFb0037099},
)
@inproceedings(BrunelGMZ14,
 author       = {Alo{\"{\i}}s Brunel and Marco Gaboardi and Damiano Mazza and Steve Zdancewic},
 year         = {2014},
 title        = {A Core Quantitative Coeffect Calculus},
 editor       = {Zhong Shao},
 booktitle    = {Programming Languages and Systems - 23rd European Symposium on Programming, {ESOP} 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2014, Grenoble, France, April 5-13, 2014, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {8410},
 publisher    = {Springer},
 pages        = {351--370},
 doi          = {10.1007/978-3-642-54833-8\_19},
)
@article(bhkm12,
 author       = {Nick Benton and Chung-Kil Hur and Andrew Kennedy and Conor McBride},
 year         = {2012},
 title        = {Strongly typed term representations in Coq},
 journal      = {J. of Autom Reasoning},
 volume       = {49},
 number       = {2},
 doi          = {10.1007/s10817-011-9219-0},
)
@article(ChaudhuriLR19,
 author       = {Kaustuv Chaudhuri and Leonardo Lima and Giselle Reis},
 year         = {2019},
 title        = {Formalized meta-theory of sequent calculi for linear logics},
 journal      = {Theor. Comput. Sci.},
 volume       = {781},
 pages        = {24--38},
 doi          = {10.1016/j.tcs.2019.02.023},
)
@article(crary10,
 author       = {Karl Crary},
 year         = {2010},
 title        = {Higher-Order Representation of Substructural Logics},
 journal      = {SIGPLAN Not.},
 volume       = {45},
 number       = {9},
 pages        = {131\IeC{\textendash}142},
 doi          = {10.1145/1932681.1863565},
)
@inproceedings(GhicaS14,
 author       = {Dan R. Ghica and Alex I. Smith},
 year         = {2014},
 title        = {Bounded Linear Types in a Resource Semiring},
 editor       = {Zhong Shao},
 booktitle    = {Programming Languages and Systems - 23rd European Symposium on Programming, {ESOP} 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2014, Grenoble, France, April 5-13, 2014, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {8410},
 publisher    = {Springer},
 pages        = {331--350},
 doi          = {10.1007/978-3-642-54833-8\_18},
)
@unpublished(laurent18,
 author       = {Olivier Laurent},
 year         = {2018},
 title        = {Preliminary Report on the Yalla Library},
 url          = {https://perso.ens-lyon.fr/olivier.laurent/yalla/},
 note         = {Coq Workshop},
)
@inproceedings(LicataSR17,
 author       = {Daniel R. Licata and Michael Shulman and Mitchell Riley},
 year         = {2017},
 title        = {A Fibrational Framework for Substructural and Modal Logics},
 booktitle    = {{FSCD} 2017},
 pages        = {25:1--25:22},
 doi          = {10.4230/LIPIcs.FSCD.2017.25},
)
@misc(rensub05,
 author       = {Conor McBride},
 year         = {2005},
 title        = {Type-preserving renaming and substitution},
 url          = {http://www.strictlypositive.org/ren-sub.pdf},
)
@article(Granule18,
 author       = {Dominic Orchard and Vilem{-}Benjamin Liepelt and Harley Eades III},
 year         = {2019},
 title        = {Quantitative program reasoning with graded modal types},
 journal      = {Proc. {ACM} Program. Lang.},
 volume       = {3},
 number       = {{ICFP}},
 pages        = {110:1--110:30},
 doi          = {10.1145/3341714},
)
@inproceedings(judgmental,
 author       = {Frank Pfenning and Rowan Davies},
 year         = {2001},
 title        = {A judgmental reconstruction of modal logic},
 volume       = {11},
 pages        = {511--540},
 doi          = {10.1017/S0960129501003322},
)
@inproceedings(PetricekOM14,
 author       = {Tomas Petricek and Dominic A. Orchard and Alan Mycroft},
 year         = {2014},
 title        = {Coeffects: a calculus of context-dependent computation},
 editor       = {Johan Jeuring and Manuel M. T. Chakravarty},
 booktitle    = {Proceedings of the 19th {ACM} {SIGPLAN} international conference on Functional programming, Gothenburg, Sweden, September 1-3, 2014},
 publisher    = {{ACM}},
 pages        = {123--135},
 doi          = {10.1145/2628136.2628160},
)
@unpublished(power99,
 author       = {James Power and Caroline Webster},
 year         = {1999},
 title        = {Working with Linear Logic in Coq},
 note         = {12th International Conference on Theorem Proving in Higher Order Logics (Work-in-progress paper)},
)
@inproceedings(RPKV20,
 author       = {Arjen Rouvoet and Bach Poulsen, Casper and Robbert Krebbers and Eelco Visser},
 year         = {2020},
 title        = {Intrinsically-Typed Definitional Interpreters for Linear, Session-Typed Languages},
 booktitle    = {CPP 2020},
 pages        = {284--298},
 doi          = {10.1145/3372885.3373818},
)
@inproceedings(reed10distance,
 author       = {Jason Reed and Benjamin C. Pierce},
 year         = {2010},
 title        = {Distance makes the types grow stronger: a calculus for differential privacy},
 editor       = {Paul Hudak and Stephanie Weirich},
 booktitle    = {Proceeding of the 15th {ACM} {SIGPLAN} international conference on Functional programming, {ICFP} 2010, Baltimore, Maryland, USA, September 27-29, 2010},
 publisher    = {{ACM}},
 pages        = {157--168},
 doi          = {10.1145/1863543.1863568},
)
@article(skew,
 author       = {Korn{\'{e}}l Szlach{\'{a}}nyi},
 year         = {2012},
 title        = {Skew-monoidal categories and bialgebroids},
 journal      = {Advances in Mathematics},
 volume       = {231},
 number       = {3-4},
 pages        = {1694--1730},
 doi          = {10.1016/j.aim.2012.06.027},
)
@inproceedings(wadler91use,
 author       = {Philip Wadler},
 year         = {1992},
 title        = {There's no substitute for linear logic},
 booktitle    = {8th International Workshop on the Mathematical Foundations of Programming Semantics},
)
@inproceedings(XavierORN18,
 author       = {Bruno Xavier and Carlos Olarte and Giselle Reis and Vivek Nigam},
 year         = {2017},
 title        = {Mechanizing Focused Linear Logic in Coq},
 booktitle    = {12th Workshop on Logical and Semantic Frameworks, with Applications},
 series       = {ENTCS},
 volume       = {338},
 publisher    = {Elsevier},
 pages        = {219--236},
 doi          = {10.1016/j.entcs.2018.10.014},
)