1. Abramsky, Samson and Tzevelekos, Nikos. 2011. Introduction to Categories and Categorical Logic. Oxford University Computing Laboratory. ArXiv : 1102.1313.
2. Amadio, Roberto and Curien, Pierre-Louis. 1996. Domains and Lambda-Calculi. Cambridge: Cambridge University Press.
3. Asperti, Andrea. 1998. “Light affine logic” . In Proc. 13th IEEE Annual Symp. on Logic in Computer Science 300-308. Washington: IEEE Computer Society.
4. Asperti, Andrea and Roversi, Luca. 2002. “Intuitionistic Light Affine Logic” . ACM Trans. Comput. Logic 3 (1): 137-175. DOI: 10.1145/504077.504081
5. Awodey, Steve. 1996. “Structure in mathematics and logic: A categorical perspective” . Philosophia Mathematica 4 (3): 209-237. DOI: 10.1093/philmat/4.3.209
6. Awodey, Steve. 2008. Category Theory (II edition). Oxford: Oxford University Press.
7. Baillot, Patrick. 2004. “Type inference for light affine logic via constraints on words” . Theoretical Computer Science 328 (3): 289-323. DOI: 10.1016/j.tcs.2004.08.014
8. Baillot, Patrick and Mogbil, Virgile. 2004. “Soft lambda-Calculus: A Language for Polynomial Time Computation” . In I. Walukiewicz (editors) Foundations of Software Science and Computation Structures 27-41. FoSSaCS 2004. Lecture Notes in Computer Science 2987. Berlin: Springer. DOI: 10.1007/978-3-540-24727-2_4
9. Barendregt, Henk P. 1984. The Lambda Calculus: Its Syntax and Semantics, second, revised edition. Amsterdam: North-Holland.
10. Bellantoni, Stephen and Cook, Stephen. 1992. “A new recursion-theoretic characterization of the polytime functions”. Computational Complexity 2: 97-110. DOI: 10.1007/BF01201998
11. Bishop, Erret. 1970. “Mathematics as a numerical language” In A. Kino, J. Myhill and R. E. Vesley (editors) Intuitionism and Proof Theory 53-71. Amsterdam: North-Holland. DOI: 10.1007/978-1-4020-8926-8_13
12. Barendregt, Henk P. 1992. “Representing undefined in Lambda calculus” . Journal of Func- tional Programming 2 (3): 367-374. DOI: 10.1017/S0956796800000447
13. Church, Alonso. 1936. “An unsolvable Problem of Elementary Number Theory”. American Journal of Mathematics 58 (2): 345-363. DOI: 10.2307/2371045
14. Crole, Roy. 1994. Categories for Types. Cambridge: Cambridge University Press. DOI: 10.1017/CBO9781139172707
15. Girard, Jean-Yves and Lafont, Yves and Taylor, Paul. 1989. Proofs and types. Cambridge: Cambridge University Press.
16. Gödel, Kurt. 1958. “Über eine bisher noch nicht benützte Erweiterung des finiten Standpunk- tes” . Dialectica 12 (3): 280.
17. Gödel, Kurt. 1972. “On an Extension of Finitary Mathematics Which Has Not Yet Been Used” . Revised and expanded English version of 1958, first published in Gödel’s Collected Works (1986-2005) II: 271-280.
18. Harper, Robert. 2011. “Existential Type” . https://existentialtype.wordpress.com/2011/03/27/the- Holy-trinity/
19. Lafont, Yves. 2004. “Soft linear logic and polynomial time” . Theoretical Computer Science, 318 (1-2): 163-180. DOI: 10.1016/j.tcs.2003.10.018
20. Lambek, Joachim and Scott, Philip J. 1986. Introduction to Higher-Order Categorical Logic. Cambridge: Cambridge University Press.
21. Leivant, Daniel and Marion, Jean-Yves. 1993. “Lambda-calculus characterisations of polytime”. Fundamenta Informaticae 19: 167-184. DOI: 10.3233/FI-1993-191-207
22. Krivine, Jean Louis. 1993. Lambda-calculus, Types and Models. London: Ellis Horwood.
23. Nerode, Anil and Odifreddi, Piergiorgio. 1990. Lambda Calculi and Constructive Logics. Mathematical Sciences Institute, Cornell University.
24. Schwichtenberg, Helmut. 1976. “Definierbare Funktionen im Lambda-Kalkul mit Typen”. Archiv Logik Grundlagenforsch. 17: 113-114.
25. Sørensen, Morten Heine and Urzyczyin, Pavel. 2006. Lectures on the Curry-Howard Isomor- phism. Amsterdam: Elsevier. DOI: 10.1016/S0049-237X(06)80005-4
26. Statman, Richard. 1979. “The typed λ-calculus is not elementary recursive.”Theoretical Com- puter Science 9(1): 73-81. DOI: 10.1016/0304-3975(79)90007-0
27. Statman, Richard. 1979“ . Intuitionistic propositional logic is polynomial-space complete”. Theoretical Computer Science 9 : 67-72. DOI: 10.1016/0304-3975(79)90006-9
28. Takahashi, Masako. 1995. “Parallel Reductions in λ-Calculus ”. Information and Computation 118 (1): 120-127. DOI: 10.1006/inco.1995.1057
29. Troelstra, Anne S. and Schwichtenberg, Helmut. 2000. Basic proof theory. Cambridge: Cam- bridge University Press. DOI: 10.1017/cbo9781139168717
30. Wadsworth, Christopher P. 1971. Semantics and Pragmatics of the Lambda-Calculus. Disser- tation. Oxford University.

Chapter Information

Bibliographic Information