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