@inproceedings(DBLP:conf/popl/AbadiCCL90,
 author       = {Mart{\'{\i}}n Abadi and Luca Cardelli and Pierre{-}Louis Curien and Jean{-}Jacques L{\'{e}}vy},
 year         = {1990},
 title        = {Explicit Substitutions},
 editor       = {Frances~E. Allen},
 booktitle    = {Conference Record of the Seventeenth Annual {ACM} Symposium on Principles of Programming Languages, San Francisco, California, USA, January 1990},
 publisher    = {{ACM} Press},
 pages        = {31--46},
 doi          = {10.1145/96709.96712},
)
@inproceedings(DBLP:journals/entcs/Accattoli18,
 author       = {Beniamino Accattoli},
 year         = {2017},
 title        = {(In)Efficiency and Reasonable Cost Models},
 editor       = {Sandra Alves and Renata Wasserman},
 booktitle    = {12th Workshop on Logical and Semantic Frameworks, with Applications, {LSFA} 2017, Bras{\'{\i}}lia, Brazil, September 23-24, 2017},
 series       = {Electronic Notes in Theoretical Computer Science},
 volume       = {338},
 publisher    = {Elsevier},
 pages        = {23--43},
 doi          = {10.1016/j.entcs.2018.10.003},
)
@inproceedings(DBLP:conf/rta/AccattoliL12,
 author       = {Beniamino Accattoli and Ugo~Dal Lago},
 year         = {2012},
 title        = {On the Invariance of the Unitary Cost Model for Head Reduction},
 editor       = {Ashish Tiwari},
 booktitle    = {23rd International Conference on Rewriting Techniques and Applications (RTA'12) , {RTA} 2012, May 28 - June 2, 2012, Nagoya, Japan},
 series       = {LIPIcs},
 volume       = {15},
 publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
 pages        = {22--37},
 doi          = {10.4230/LIPIcs.RTA.2012.22},
)
@book(barendregt2013lambda,
 author       = {Henk Barendregt and Wil Dekkers and Richard Statman},
 year         = {2013},
 title        = {Lambda calculus with types},
 publisher    = {Cambridge University Press},
 doi          = {10.1017/CBO9781139032636},
)
@inproceedings(Bloo95preservationof,
 author       = {Roel Bloo and Kristoffer~H. Rose},
 year         = {1995},
 title        = {Preservation of Strong Normalisation in Named Lambda Calculi with Explicit Substitution and Garbage Collection},
 booktitle    = {IN CSN-95: COMPUTER SCIENCE IN THE NETHERLANDS},
 pages        = {62--72},
)
@book(brauner1996cut,
 author       = {Torben Bra{\"u}ner and De~Paiva, Valeria},
 year         = {1996},
 title        = {Cut-elimination for full intuitionistic linear logic},
 volume       = {10},
 publisher    = {University of Cambridge, Computer Laboratory},
 doi          = {10.7146/brics.v3i10.19973},
)
@article(curzi2019type,
 author       = {Gianluca Curzi and Luca Roversi},
 year         = {2020},
 title        = {A type-assignment of linear erasure and duplication},
 journal      = {Theoretical Computer Science},
 volume       = {837},
 pages        = {26--53},
 doi          = {10.1016/j.tcs.2020.05.001},
)
@article(curzi2020probabilistic,
 author       = {Gianluca Curzi and Luca Roversi},
 year         = {2020},
 title        = {Probabilistic Soft Type Assignment},
 journal      = {arXiv preprint arXiv:2007.01733},
)
@article(diaz2013non,
 author       = {D{\'\i}az-Caro, Alejandro and Gilles Dowek},
 year         = {2013},
 title        = {Non determinism through type isomorphism},
 journal      = {arXiv preprint arXiv:1303.7334},
)
@article(gaboardi2009light,
 author       = {Marco Gaboardi and Della~Rocca, Simona~Ronchi},
 year         = {2009},
 title        = {From light logics to type assignments: a case study},
 journal      = {Logic Journal of the IGPL},
 volume       = {17},
 number       = {5},
 pages        = {499--530},
 doi          = {10.1093/jigpal/jzp019},
)
@article(gaboardi2008soft,
 author       = {Marco Gaboardi and Jean-Yves Marion and Della~Rocca, Simona~Ronchi},
 year         = {2008},
 title        = {Soft linear logic and polynomial complexity classes},
 journal      = {Electronic Notes in Theoretical Computer Science},
 volume       = {205},
 pages        = {67--87},
 doi          = {10.1016/j.entcs.2008.03.066},
)
@incollection(girard2017proof,
 author       = {Jean-Yves Girard},
 year         = {2017},
 title        = {Proof-nets: the parallel syntax for proof-theory},
 booktitle    = {Logic and Algebra},
 publisher    = {Routledge},
 pages        = {97--124},
 doi          = {10.1201/9780203748671-4},
)
@inproceedings(girard1987linear,
 author       = {Jean-Yves Girard and Yves Lafont},
 year         = {1987},
 title        = {Linear logic and lazy computation},
 booktitle    = {International Joint Conference on Theory and Practice of Software Development},
 organization = {Springer},
 pages        = {52--66},
 doi          = {10.1007/BFb0014972},
)
@article(hindley1989bck,
 author       = {J~Roger Hindley},
 year         = {1989},
 title        = {BCK-combinators and linear $\lambda$-terms have types},
 journal      = {Theoretical Computer Science},
 volume       = {64},
 number       = {1},
 pages        = {97--105},
 doi          = {10.1016/0304-3975(89)90100-X},
)
@inproceedings(horne2019sub,
 author       = {Ross Horne},
 year         = {2019},
 title        = {The sub-additives: A proof theory for probabilistic choice extending linear logic},
 booktitle    = {4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
 organization = {Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik},
 doi          = {10.4230/LIPIcs.FSCD.2019.23},
)
@inproceedings(DBLP:conf/cie/LagoM06,
 author       = {Ugo~Dal Lago and Simone Martini},
 year         = {2006},
 title        = {An Invariant Cost Model for the Lambda Calculus},
 editor       = {Arnold Beckmann and Ulrich Berger and Benedikt L{\"{o}}we and John~V. Tucker},
 booktitle    = {Logical Approaches to Computational Barriers, Second Conference on Computability in Europe, CiE 2006, Swansea, UK, June 30-July 5, 2006, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {3988},
 publisher    = {Springer},
 pages        = {105--114},
 doi          = {10.1007/11780342\_11},
)
@article(mairsonlinear,
 author       = {Harry~G. Mairson},
 year         = {2004},
 title        = {Linear {L}ambda {C}alculus and {PTIME}-completeness},
 journal      = {J. Funct. Program.},
 volume       = {14},
 number       = {6},
 pages        = {623--633},
 doi          = {10.1017/S0956796804005131},
)
@inproceedings(mairson2003computational,
 author       = {Harry~G. Mairson and Kazushige Terui},
 year         = {2003},
 title        = {{O}n the {C}omputational {C}omplexity of {C}ut-{E}limination in {L}inear {L}ogic},
 editor       = {Carlo Blundo and Cosimo Laneve},
 booktitle    = {Theoretical Computer Science},
 publisher    = {Springer Berlin Heidelberg},
 address      = {Berlin, Heidelberg},
 pages        = {23--36},
 doi          = {10.1007/978-3-540-45208-9\_4},
)
@article(matsuoka2004nondeterministic,
 author       = {Satoshi Matsuoka},
 year         = {2004},
 title        = {Nondeterministic Linear Logic},
 journal      = {arXiv preprint cs/0410029},
)
@inproceedings(maurel2003nondeterministic,
 author       = {Fran{\c{c}}ois Maurel},
 year         = {2003},
 title        = {Nondeterministic light logics and NP-time},
 booktitle    = {International Conference on Typed Lambda Calculi and Applications},
 organization = {Springer},
 pages        = {241--255},
 doi          = {10.1007/3-540-44904-3\_17},
)
@inproceedings(10.5555/645892.671591,
 author       = {Paul-Andr\'{e} Melli\`{e}s},
 year         = {1995},
 title        = {Typed Lambda-Calculi with Explicit Substitutions May Not Terminate},
 booktitle    = {Proceedings of the Second International Conference on Typed Lambda Calculi and Applications},
 series       = {TLCA '95},
 publisher    = {Springer-Verlag},
 address      = {Berlin, Heidelberg},
 pages        = {328\IeC{\textendash}334},
 doi          = {10.1007/BFb0014062},
)