@book(BDS13,
 author       = {H. Barendregt and W. Dekkers and R. Statman},
 year         = {2013},
 title        = {Lambda Calculus with Types},
 publisher    = {Cambridge University Press},
 doi          = {10.1017/CBO9781139032636},
)
@book(Bar81,
 author       = {H. P. Barendregt},
 year         = {1981},
 title        = {The Lambda Calculus: Its Syntax and Semantics},
 publisher    = {North Holland},
)
@inbook(BS04,
 author       = {R. Blute and P. Scott},
 year         = {2004},
 title        = {Category Theory for Linear Logicians},
 pages        = {3--64},
 series       = {LMS Lecture Note Series},
 volume       = {316},
 publisher    = {Cambridge University Press},
 doi          = {10.2277/0521608570},
)
@book(Cro94,
 author       = {R. L. Crole},
 year         = {1994},
 title        = {Categories for Types},
 publisher    = {Cambridge University Press},
 doi          = {10.1017/CBO9781139172707},
)
@inproceedings(DM82,
 author       = {L. Damas and R. Milner},
 year         = {1982},
 title        = {Principal Type-Schemes for Functional Programs},
 booktitle    = {Conference Record of the Ninth Annual {ACM} Symposium on Principles of Programming Languages, Albuquerque, New Mexico, USA, January 1982},
 pages        = {207--212},
 doi          = {10.1145/582153.582176},
)
@article(Gir87,
 author       = {J.-Y. Girard},
 year         = {1987},
 title        = {Linear Logic},
 journal      = {Theoretical Computer Science},
 volume       = {50},
 pages        = {1--102},
 doi          = {10.1016/0304-3975(87)90045-4},
)
@book(GLT89,
 author       = {J.-Y. Girard and Y. Lafont and P. Taylor},
 year         = {1989},
 title        = {Proofs and Types},
 publisher    = {Cambridge University Press},
)
@article(Hin89,
 author       = {R. Hindley},
 year         = {1989},
 title        = {BCK-combinators and Linear $\lambda$-terms have Types},
 journal      = {Theoretical Computer Science},
 volume       = {64},
 pages        = {97--105},
 doi          = {10.1016/0304-3975(89)90100-X},
)
@inproceedings(vanHM07,
 author       = {D. Van Horn and H. G. Mairson},
 year         = {2007},
 title        = {Relating complexity and precision in control flow analysis},
 booktitle    = {Proceedings of the 12th {ACM} {SIGPLAN} International Conference on Functional Programming, {ICFP} 2007, Freiburg, Germany, October 1-3, 2007},
 pages        = {85--96},
 doi          = {10.1145/1291151.1291166},
)
@book(LS88,
 author       = {J. Lambek and P. Scott},
 year         = {1988},
 title        = {Introduction to Higher-Order Categorical Logic},
 publisher    = {Cambridge University Press},
)
@article(MRA93,
 author       = {I. Mackie and L. Rom\'{a}n and S. Abramsky},
 year         = {1993},
 title        = {An Internal Language for Autonomous Categories},
 journal      = {Applied Categorical Structures},
 volume       = {1},
 pages        = {311--343},
 doi          = {10.1007/BF00873993},
)
@article(Mai04,
 author       = {H. G. Mairson},
 year         = {2004},
 title        = {Linear Lambda Calculus and PTIME-completeness},
 journal      = {Journal of Functional Programing},
 volume       = {14},
 number       = {6},
 pages        = {623--633},
 doi          = {10.1017/S0956796804005131},
)
@article(Mat07,
 author       = {S. Matsuoka},
 year         = {2007},
 title        = {Weak Typed B\"{o}hm Theorem on IMLL},
 journal      = {Annals of Pure and Applied Logic},
 volume       = {145},
 number       = {1},
 pages        = {37--90},
 doi          = {10.1016/j.apal.2006.06.001},
)
@inproceedings(Mat15,
 author       = {S. Matsuoka},
 year         = {2015},
 title        = {A New Proof of P-time Completeness},
 editor       = {Geoff Sutcliffe Ansgar Fehnker, Annabelle McIver and Andrei Voronkov},
 booktitle    = {LPAR-20. 20th International Conferences on Logic for Programming, Artificial Intelligence and Reasoning - Short Presentations},
 series       = {EPiC Series in Computer Science},
 volume       = {35},
 publisher    = {EasyChair},
 pages        = {119--130},
 url          = {http://www.easychair.org/publications/download/A_New_Proof_of_P-time_Completeness_of_Linear_Lambda_Calculus},
)
@book(MTHM97,
 author       = {R. Milner and M. Tofte and R. Harper and D. MacQueen},
 year         = {1997},
 title        = {The Definition of Standard ML (Revised)},
 publisher    = {MIT Press},
)
@inbook(Sta80,
 author       = {R. Statman},
 year         = {1980},
 title        = {On the existence of closed terms in the typed $\lambda$-calculs. I},
 pages        = {511--534},
 publisher    = {Academic Press},
)
@article(Sta83,
 author       = {R. Statman},
 year         = {1983},
 title        = {$\lambda$-definable Functionals and $\beta\eta $-conversion},
 journal      = {Archiv f\"{u}r mathematische Logik und Grundlagenforschung},
 volume       = {23},
 pages        = {21--26},
 doi          = {10.1007/BF02023009},
)
@techreport(SD92,
 author       = {R. Statman and G. Dowek},
 year         = {1992},
 title        = {On Statman's Finite Completeness Theorem},
 type         = {Technical Report},
 institution  = {Carnegie Mellon University},
 note         = {CMU-CS-92-152},
)
@book(Tro92,
 author       = {A. S. Troelstra},
 year         = {1992},
 title        = {Lectures on Linear Logic},
 publisher    = {CSLI},
)