H. P. Barendregt (1984):
The Lambda Calculus Its Syntax and Semantics,
revised edition 103.
North Holland.
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.
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 https://doi.org/10.1017/S147106841700045X.
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.
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.
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.
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).
Roy Dyckhoff (1992):
Contraction-free sequent calculi for intuitionistic logic.
Journal of Symbolic Logic 57(3),
pp. 795â807,
doi:10.2307/2275431.
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.
Jean-Yves Girard (1987):
Linear logic.
Theoretical computer science 50(1),
pp. 1–101,
doi:10.1016/0304-3975(87)90045-4.
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.
Katarzyna Grygiel & Pierre Lescanne (2013):
Counting and generating lambda terms.
J. Funct. Program. 23(5),
pp. 594–628,
doi:10.1017/S0956796813000178.
J. Roger Hindley (1997):
Basic Simple Type Theory.
Cambridge University Press,
New York, NY, USA,
doi:10.1017/CBO9780511608865.
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.
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.
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.
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 http://papers.nips.cc/paper/7632-deepproblog-neural-probabilistic-logic-programming.pdf.
Grigorii E. Mints (1992):
Closed categories and the theory of proofs.
In: Selected Papers in Proof Theory.
Bibliopolis,
doi:10.1007/BF01404107.
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.
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 http://papers.nips.cc/paper/6969-end-to-end-differentiable-proving.pdf.
H Schellinx (1994):
The noble art of linear decorating. ILLC Dissertation Series, 1994-1.
Institute for Language, Logic and Computation, University of Amsterdam.
N. J. A. Sloane (2020):
The On-Line Encyclopedia of Integer Sequences..
Published electronically at https://oeis.org/.
R P Stanley (1986):
Enumerative Combinatorics.
Wadsworth Publ. Co.,
Belmont, CA, USA.
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.
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.
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.
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.
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.
Philip Wadler (2015):
Propositions as types.
Commun. ACM 58,
pp. 75–84,
doi:10.1145/2699407.
Noam Zeilberger (2015):
Balanced polymorphism and linear lambda calculus, talk at TYPES'15.
http://noamz.org/papers/linprin.pdf.