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