@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}},
)