@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},
)