1. H. P. Barendregt (1984): The Lambda Calculus Its Syntax and Semantics, revised edition 103. North Holland.
  2. Maciej Bendkowski, Katarzyna Grygiel & Paul Tarau (2017): Boltzmann Samplers for Closed Simply-Typed Lambda Terms. In: Yuliya Lierler & Walid Taha: Practical Aspects of Declarative Languages - 19th International Symposium, PADL 2017, Paris, France, January 16-17, 2017, Proceedings, Lecture Notes in Computer Science 10137. Springer, pp. 120–135, doi:10.1007/978-3-319-51676-9. , Best student paper award.
  3. Maciej Bendkowski, Katarzyna Grygiel & Paul Tarau (2018): Random generation of closed simply typed λ-terms: A synergy between logic programming and Boltzmann samplers. TPLP 18(1), pp. 97–119. Available at
  4. Nick Benton, Gavin Bierman, Valeria De Paiva & Martin Hyland (1993): A term calculus for intuitionistic linear logic. In: International Conference on Typed Lambda Calculi and Applications. Springer, pp. 75–90, doi:10.1007/BFb0037099.
  5. Jean-Philippe Bernardy, Mathieu Boespflug, Ryan R. Newton, Simon Peyton Jones & Arnaud Spiwack (2018): Linear Haskell: practical linearity in a higher-order polymorphic language. Proc. ACM Program. Lang. 2(POPL), pp. 5:1–5:29, doi:10.1145/3158093.
  6. O. Bodini, D. Gardy & A. Jacquot (2013): Asymptotics and random sampling for BCI and BCK lambda terms. Theoretical Computer Science 502, pp. 227 – 238, doi:10.1016/j.tcs.2013.01.008.
  7. O. Bodini & P. Tarau (2017): On Uniquely Closable and Uniquely Typable Skeletons of Lambda Terms. CoRR abs/1709.04302. Available at, doi:10.1007/978-3-319-94460-9_15.
  8. René David, Christophe Raffalli, Guillaume Theyssier, Katarzyna Grygiel, Jakub Kozik & Marek Zaionc (2009): Some properties of random lambda terms. Logical Methods in Computer Science 9(1).
  9. Honghua Dong, Jiayuan Mao, Tian Lin, Chong Wang, Lihong Li & Denny Zhou (2019): Neural Logic Machines. Available at
  10. Roy Dyckhoff (1992): Contraction-free sequent calculi for intuitionistic logic. Journal of Symbolic Logic 57(3), pp. 795–807, doi:10.2307/2275431.
  11. Antoine Genitrini, Jakub Kozik & Marek Zaionc (2007): Intuitionistic vs. Classical Tautologies, Quantitative Comparison. In: Marino Miculan, Ivan Scagnetto & Furio Honsell: Types for Proofs and Programs, International Conference, TYPES 2007, Cividale del Friuli, Italy, May 2-5, 2007, Revised Selected Papers, Lecture Notes in Computer Science 4941. Springer, pp. 100–109, doi:10.1007/978-3-540-68103-8_7.
  12. Jean-Yves Girard (1987): Linear logic. Theoretical computer science 50(1), pp. 1–101, doi:10.1016/0304-3975(87)90045-4.
  13. Georges Gonthier, Martín Abadi & Jean-Jacques Lévy (1992): The geometry of optimal lambda reduction. In: Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp. 15–26, doi:10.1145/143165.143172.
  14. Katarzyna Grygiel & Pierre Lescanne (2013): Counting and generating lambda terms. J. Funct. Program. 23(5), pp. 594–628, doi:10.1017/S0956796813000178.
  15. J. Roger Hindley (1997): Basic Simple Type Theory. Cambridge University Press, New York, NY, USA, doi:10.1017/CBO9780511608865.
  16. W.A. Howard (1980): The Formulae-as-types Notion of Construction. In: J.P. Seldin & J.R. Hindley: To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. Academic Press, London, pp. 479–490.
  17. S.C. Kleene (1952): Introduction to Metamathematics. Bibliotheca Mathematica. Wolters-Noordhoff. Available at
  18. A.P. Kopylov (1995): Decidability of Linear Affine Logic. In: Dexter Kozen: Proceedings of the Tenth Annual IEEE Symp. on Logic in Computer Science, LICS 1995. IEEE Computer Society Press, pp. 496–504, doi:10.1006/inco.1999.2834.
  19. Pierre Lescanne (2018): Quantitative Aspects of Linear and Affine Closed Lambda Terms. ACM Trans. Comput. Log. 19(2), pp. 9:1–9:18, doi:10.1145/3173547.
  20. Robin Manhaeve, Sebastijan Dumancic, Angelika Kimmig, Thomas Demeester & Luc De Raedt (2018): DeepProbLog: Neural Probabilistic Logic Programming. In: S. Bengio, H. Wallach, H. Larochelle, K. Grauman, N. Cesa-Bianchi & R. Garnett: Advances in Neural Information Processing Systems 31. Curran Associates, Inc., pp. 3749–3759. Available at
  21. Grigorii E. Mints (1992): Closed categories and the theory of proofs. In: Selected Papers in Proof Theory. Bibliopolis, doi:10.1007/BF01404107.
  22. Carlos Olarte, Valeria de Paiva, Elaine Pimentel & Giselle Reis (2018): The ILLTP Library for Intuitionistic Linear Logic. In: Thomas Ehrhard, Maribel Fernández, Valeria de Paiva & Lorenzo Tortora de Falco: Proceedings Joint International Workshop on Linearity & Trends in Linear Logic and Applications, Linearity-TLLA@FLoC 2018, Oxford, UK, 7-8 July 2018, EPTCS 292, pp. 118–132, doi:10.4204/EPTCS.292.7.
  23. Tim Rocktäschel & Sebastian Riedel (2017): End-to-end Differentiable Proving. In: I. Guyon, U. V. Luxburg, S. Bengio, H. Wallach, R. Fergus, S. Vishwanathan & R. Garnett: Advances in Neural Information Processing Systems 30. Curran Associates, Inc., pp. 3788–3800. Available at
  24. H Schellinx (1994): The noble art of linear decorating. ILLC Dissertation Series, 1994-1. Institute for Language, Logic and Computation, University of Amsterdam.
  25. N. J. A. Sloane (2020): The On-Line Encyclopedia of Integer Sequences.. Published electronically at
  26. R P Stanley (1986): Enumerative Combinatorics. Wadsworth Publ. Co., Belmont, CA, USA.
  27. Richard Statman (1979): Intuitionistic Propositional Logic is Polynomial-Space Complete. Theor. Comput. Sci. 9, pp. 67–72, doi:10.1016/0304-3975(79)90006-9.
  28. Paul Tarau (2015): On a Uniform Representation of Combinators, Arithmetic, Lambda Terms and Types. In: Elvira Albert: PPDP'15: Proceedings of the 17th international ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming. ACM, New York, NY, USA, pp. 244–255, doi:10.1145/2790449.2790526.
  29. Paul Tarau (2017): A Hiking Trip Through the Orders of Magnitude: Deriving Efficient Generators for Closed Simply-Typed Lambda Terms and Normal Forms. In: Manuel V Hermenegildo & Pedro Lopez-Garcia: Logic-Based Program Synthesis and Transformation: 26th International Symposium, LOPSTR 2016, Edinburgh, UK, Revised Selected Papers. Springer LNCS, volume 10184, pp. 240–255, doi:10.1007/978-3-319-63139-4_14. , Best paper award.
  30. Paul Tarau (2018): On k-colored Lambda Terms and their Skeletons. In: Francesco Calimeri, Kevin W. Hamlen & Nicola Leone: Practical Aspects of Declarative Languages - 20th International Symposium, PADL 2018, Los Angeles, CA, USA, January 8-9, 2018, Proceedings, Lecture Notes in Computer Science 10702. Springer, pp. 116–131, doi:10.1007/978-3-319-73305-0_8.
  31. Paul Tarau (2019): A Combinatorial Testing Framework for Intuitionistic Propositional Theorem Provers. In: José Júlio Alferes & Moa Johansson: Practical Aspects of Declarative Languages - 21th International Symposium, PADL 2019, Lisbon, Portugal, January 14-15, 2019, Proceedings, Lecture Notes in Computer Science 11372. Springer, pp. 115–132, doi:10.1007/978-3-030-05998-9_8.
  32. Philip Wadler (2015): Propositions as types. Commun. ACM 58, pp. 75–84, doi:10.1145/2699407.
  33. Noam Zeilberger (2015): Balanced polymorphism and linear lambda calculus, talk at TYPES'15.

Comments and questions to:
For website issues: