1. H. Barendregt, W. Dekkers & R. Statman (2013): Lambda Calculus with Types. Cambridge University Press, doi:10.1017/CBO9781139032636.
  2. H. P. Barendregt (1981): The Lambda Calculus: Its Syntax and Semantics. North Holland.
  3. 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.
  4. R. L. Crole (1994): Categories for Types. Cambridge University Press, doi:10.1017/CBO9781139172707.
  5. 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.
  6. J.-Y. Girard (1987): Linear Logic. Theoretical Computer Science 50, pp. 1–102, doi:10.1016/0304-3975(87)90045-4.
  7. J.-Y. Girard, Y. Lafont & P. Taylor (1989): Proofs and Types. Cambridge University Press.
  8. 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.
  9. 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.
  10. J. Lambek & P. Scott (1988): Introduction to Higher-Order Categorical Logic. Cambridge University Press.
  11. 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.
  12. H. G. Mairson (2004): Linear Lambda Calculus and PTIME-completeness. Journal of Functional Programing 14(6), pp. 623–633, doi:10.1017/S0956796804005131.
  13. 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.
  14. 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
  15. R. Milner, M. Tofte, R. Harper & D. MacQueen (1997): The Definition of Standard ML (Revised). MIT Press.
  16. R. Statman (1980): On the existence of closed terms in the typed λ-calculs. I, pp. 511–534. Academic Press.
  17. R. Statman (1983): λ-definable Functionals and βη-conversion. Archiv für mathematische Logik und Grundlagenforschung 23, pp. 21–26, doi:10.1007/BF02023009.
  18. R. Statman & G. Dowek (1992): On Statman's Finite Completeness Theorem. Technical Report. Carnegie Mellon University. CMU-CS-92-152.
  19. A. S. Troelstra (1992): Lectures on Linear Logic. CSLI.

Comments and questions to:
For website issues: