Full Bibliography

[Alessi et al., 2006] Alessi, F., Barbanera, F., and Dezani-Ciancaglini, M. (2006). Intersection types and lambda models. Theoretical Computer Science, 355(2):108–126.

[Alessi et al., 2004] Alessi, F., Dezani-Ciancaglini, M., and Lusin, S. (2004). Intersection types and domain operators. Theoretical Computer Science, 316(1–3):25–47.

[Alessi and Lusin, 2002] Alessi, F. and Lusin, S. (2002). Simple easy terms. In van Bakel, S., editor, Intersection Types and Related Systems, volume 70 of Electronic Notes in Computer Science. Elsevier.

[Altenkirch et al., 2001] Altenkirch, T., Dybjer, P., Hofmann, M., and Scott, P. (2001). Normalization by evaluation for typed lambda calculus with coproducts. In Logic in Computer Science, pages 303–310. IEEE Computer Society Press.

[Altenkirch and Uustalu, 2004] Altenkirch, T. and Uustalu, T. (2004). Normalization by evaluation for $λ →2$ . In Functional and Logic Programming, volume 2998 of Lecture Notes in Computer Science, pages 260–275.

[Anderson, 1960] Anderson, A. R. (1960). Entailment shorn of modality. Journal of Symbolic Logic, 25:388. (Abstract).

[Anderson and Belnap, 1975] Anderson, A. R. and Belnap, N. D. (1975). Entailment. The Logic of Relevance and Necessity, Volume 1. Princeton University Press, U.S.A.

[Anderson et al., 1992] Anderson, A. R., Belnap, N. D., and Dunn, J. M. (1992). Entailment. The Logic of Relevance and Necessity, Volume 2. Princeton University Press, U.S.A.

[Barendregt, 1975] Barendregt, H. (1975). Open problems. In [Böhm, 1975], pages 367–370.

[Barendregt, 1984] Barendregt, H. (1984). The Lambda Calculus. Its Syntax and Semantics. North-Holland, second edition.

[Barendregt et al., 1983] Barendregt, H., Coppo, M., and Dezani-Ciancaglini, M. (1983). A ﬁlter lambda model and the completeness of type assignment. Journal of Symbolic Logic, 48(4):931–940.

[Barendregt and Manzonetto, 2013] Barendregt, H. and Manzonetto, G. (2013). Turing’s contributions to lambda calculus. In Cooper, S. B. and van Leeuwen, J., editors, Alan Turing: His Work and Impact, pages 139–143. Elsevier.

[Barthe, 1995] Barthe, G. (1995). Extensions of Pure Type Systems. In [Dezani-Ciancaglini and Plotkin, 1995], pages 16–31.

[Barthe, 1998a] Barthe, G. (1998a). The semi-full closure of Pure Type Systems. In Brim, L., Gruska, J., and Zlatuska, J., editors, Proceedings of MFCS’98, volume 1450 of Lecture Notes in Computer Science, pages 316–325. Springer-Verlag.

[Barthe, 1998b] Barthe, G. (1998b). Type-checking injective pure type systems. Journal of Functional Programming, 9:675–698.

[Barthe et al., 2001] Barthe, G., Hatcliff, J., and Sørensen, M. H. (2001). Weak normalization implies strong normalization in a class of non-dependent pure type systems. Theoretical Computer Science, 269(1–2):317–361.

[Berarducci, 1996] Berarducci, A. (1996). Inﬁnite $λ$ -calculus and non-sensible models. In Ursini, A. and Aglianò, P., editors, Logic and Algebra (Pontignano, 1994), pages 339–377. Dekker.

[Bergstra and Klop, 1980] Bergstra, J. A. and Klop, J. W. (1980). Invertible terms in the lambda calculus. Theoretical Computer Science, 11:19–37.

[Berline, 2000] Berline, C. (2000). The lambda-calculus and its webbed models. Theoretical Computer Science, 249(1):81–161.

[Berline, 2006] Berline, C. (2006). Graph models of lambda-calculus at work, and variations. Mathematical Structures in Computer Science, 16:185–221.

[Bimbó, 2005] Bimbó, K. (2005). Types of I-free hereditary right maximal terms. Journal of Philosophical Logic, 34:607–620.

[Bimbó, 2006] Bimbó, K. (2006). Relevance logics. In Jacquette, D., editor, Philosophy of Logic, volume 5 of Handbook of the Philosophy of Science, pages 723–789. North-Holland/ Elsevier, Amsterdam.

[Bimbó and Dunn, 2013] Bimbó, K. and Dunn, J. M. (2013). On the decidability of implicational ticket entailment. Journal of Symbolic Logic, 78(1):214–236.

[Böhm, 1975] Böhm, C., editor (1975). $λ$ -Calculus and Computer Science Theory, volume 37 of Lecture Notes in Computer Science. Springer-Verlag.

[Broda and Damas, 1997] Broda, S. and Damas, L. (1997). On combinatory complete sets of proper combinators. Journal of Functional Programming, 7(6):593–612.

[Broda et al., 2004] Broda, S., Damas, L., Finger, M., and e Silva, P. S. (2004). The decidability of a fragment of BB’IW-logic. Theoretical Computer Science, 318(3):373–408.

[Carraro and Salibra, 2012] Carraro, A. and Salibra, A. (2012). Easy lambda-terms are not always simple. RAIRO - Theoretical Informatics and Applications, 46:291–314.

[Curry and Feys, 1958] Curry, H. B. and Feys, R. (1958). Combinatory Logic, Volume I. North-Holland, Amsterdam. (3rd edition 1974).

[Curry et al., 1972] Curry, H. B., Hindley, J. R., and Seldin, J. P. (1972). Combinatory Logic, Volume II. North-Holland, Amsterdam.

[David, 2009] David, R. (2009). A direct proof of the conﬂuence of combinatory strong reduction. Theoretical Computer Science, 410(42):4204–4215.

[de Vrijer, 1987] de Vrijer, R. (1987). Exactly estimating functionals and strong normalization. Indagationes Mathematicae, 49:479–493.

[de’Liguoro et al., 1992] de’Liguoro, U., Piperno, A., and Statman, R. (1992). Retracts in simply typed lambda-beta-eta-calculus. In Logic in Computer Science, pages 461–469. IEEE Computer Society Press.

[Dezani-Ciancaglini et al., 2005] Dezani-Ciancaglini, M., Honsell, F., and Motohama, Y. (2005). Compositional characterization of $λ$ -terms using intersection types. Theoretical Computer Science, 340(3):459–495.

[Dezani-Ciancaglini and Plotkin, 1995] Dezani-Ciancaglini, M. and Plotkin, G., editors (1995). Typed Lambda Calculi and Applications, volume 902 of Lecture Notes in Computer Science. Springer-Verlag.

[Di Gianantonio et al., 1995] Di Gianantonio, P., Honsell, F., and Plotkin, G. (1995). Uncountable limits and the lambda calculus. Nordic Journal of Computing, 2(2):126–145.

[Dougherty and Subrahmanyam, 2000] Dougherty, D. and Subrahmanyam, R. (2000). Equality between functionals in the presence of coproducts. Information and Computation, 157:52–83.

[Geuvers, 1993] Geuvers, H. (1993). Logics and Type Systems. PhD thesis, Nijmegen University.

[Ghani, 1995] Ghani, N. (1995). Beta-eta equality for coproducts. In [Dezani-Ciancaglini and Plotkin, 1995], pages 171–185.

[Giannini and Ronchi Della Rocca, 1994] Giannini, P. and Ronchi Della Rocca, S. (1994). A type inference algorithm for a complete stratiﬁcation of the polymorphic type discipline. Information and Computation, 110:115 – 173.

[Girard, 1986] Girard, J.-Y. (1986). The system F of variable types, ﬁfteen years later. Theoretical Computer Science, 45:159–192.

[Gørtz et al., 2003] Gørtz, I. L., Reuss, S., and Sørensen, M. H. (2003). Strong normalization from weak normalization by translation into the lambda-I-calculus. Higher Order Symbol. Comput., 16(3):253–285.

[Gutiérrez and Ruiz, 2003] Gutiérrez, F. and Ruiz, B. (2003). Cut elimination in a class of sequent calculi for pure type systems. Electronic Notes in Computer Science, 84:105–116.

[Henglein and Rehof, 1997] Henglein, F. and Rehof, J. (1997). The complexity of subtype entailment for simple types. In Logic in Computer Science, pages 352–361. IEEE Computer Society Press.

[Henglein and Rehof, 1998] Henglein, F. and Rehof, J. (1998). Constraint automata and the complexity of recursive subtype entailment. In International Colloquium on Automata, Languages, and Programming, volume 1443 of Lecture Notes in Computer Science, pages 616–627. Springer-Verlag.

[Hindley and Seldin, 1986] Hindley, J. R. and Seldin, J. P. (1986). Introduction to Combinators and $λ$ -calculus. Cambridge University Press.

[Honsell and Ronchi Della Rocca, 1992] Honsell, F. and Ronchi Della Rocca, S. (1992). An approximation theorem for topological lambda models and the topological incompleteness of lambda calculus. Journal of Computer and System Sciences, 45(1):49–75.

[Howard, 1970] Howard, W. (1970). Assignment of ordinals to terms for primitive recursive functionals of ﬁnite type. In A. Kino, J. M. and Vesley, R., editors, Intuitionism and Proof Theory: Proceedings of the Summer Conference at Buffalo N.Y. 1968, volume 60 of Studies in Logic and the Foundations of Mathematics, pages 443 – 458. Elsevier.

[Hyland, 1976] Hyland, M. (1976). A syntactic characterization of the equality in some models for the lambda calculus. J. London Math. Soc. (2), 12(3):361–370.

[Intrigila and Biasone, 2000] Intrigila, B. and Biasone, E. (2000). On the number of ﬁxed points of a combinator in lambda calculus. Mathematical Structures in Computer Science, 10(5):595–615.

[Intrigila and Statman, 2011] Intrigila, B. and Statman, R. (2011). Solution to the range problem for combinatory logic. Fundamenta Informaticae, 111(2):203–222.

[Jacopini, 1975] Jacopini, G. (1975). A condition for identifying two elements of whatever model of combinatory logic. In [Böhm, 1975], pages 213–219.

[Kennaway et al., 2005] Kennaway, J., Severi, P., Sleep, M., and de Vries, F. J. (2005). Inﬁnite rewriting: from syntax to semantics. In Processes, Terms and Cycles: Steps on the Road to Inﬁnity: Essays Dedicated to Jan Willem Klop on the Occasion of His 60th Birthday, volume 3838 of Lecture Notes in Computer Science, pages 148–172. Springer-Verlag.

[Ketema et al., 2005] Ketema, J., Klop, J. W., and van Oostrom, V. (2005). Vicious circles in orthogonal term rewriting systems. Electronic Notes in Computer Science, 124(2):65–77.

[Kurata, 2002] Kurata, T. (2002). Intersection and singleton type assignment characterizing ﬁnite Böhm-trees. Information and Computation, 178(1):1–11.

[Kurata and Takahashi, 1995] Kurata, T. and Takahashi, M. (1995). Decidable properties of intersection type systems. In [Dezani-Ciancaglini and Plotkin, 1995], pages 297–311.

[Kuśmierek, 2007] Kuśmierek, D. (2007). The inhabitation problem for rank two intersection types. In Ronchi Della Rocca, S., editor, Typed Lambda Calculi and Applications, volume 4583 of Lecture Notes in Computer Science, pages 240–254. Springer-Verlag.

[Leivant, 1983] Leivant, D. (1983). Polymorphic type inference. In Symposium on Principles of Programming Languages, pages 88–98. ACM Press.

[Malecki, 1997] Malecki, S. (1997). Proofs in system $Fω$ can be done in system $1 Fω$ . In van Dalen, D. and Bezem, M., editors, Computer Science Logic, volume 1258 of Lecture Notes in Computer Science, pages 297–315. Springer-Verlag.

[McCune and Wos, 1991] McCune, W. and Wos, L. (1991). The absence and the presence of ﬁxed point combinators. Theoretical Computer Science, 87:221–228.

[Mendler, 1987] Mendler, N. (1987). Recursive types and type constraints in second-order lambda calculus. In Logic in Computer Science, pages 30–36. IEEE Computer Society Press.

[Mendler, 1991] Mendler, N. (1991). Inductive types and type constraints in the second-order lambda calculus. Annals of Pure and Applied Logic, 51(1-2):159–172.

[Minari, 2009] Minari, P. (2009). A solution to Curry and Hindley’s problem on combinatory strong reduction. Archive for Mathematical Logic, 43(2):159–184.

[Niehren and Priesnitz, 2003] Niehren, J. and Priesnitz, T. (2003). Non-structural subtype entailment in automata theory. Information and Computation, 186(2):319–354.

[Padovani, 2001] Padovani, V. (2001). Retracts in simple types. In Abramsky, S., editor, Typed Lambda Calculi and Applications, volume 2044 of Lecture Notes in Computer Science, pages 376–384. Springer-Verlag.

[Padovani, 2013] Padovani, V. (2013). Ticket entailment is decidable. Mathematical Structures in Computer Science, 23(3):568–607.

[Poll, 1998] Poll, E. (1998). Theoretical pearl: Expansion postponement for normalising pure type systems. Journal of Functional Programming, 8:89–96.

[Pollack, 1992] Pollack, R. (1992). Typechecking in Pure Type Systems. In Informal Proceedings of the 1992 Workshop on Types for Proofs and Programs, Bastad, Sweden, pages 271–288.

[Polonsky, 2012] Polonsky, A. (2012). The range property fails for H. Journal of Logic and Computation, 77(4):1195–1210.

[Pólya, 2004] Pólya, G. (2004). How to Solve It: A New Aspect of Mathematical Method. Penguin mathematics. Princeton University Press. Expanded version of the 1988 edition, with a new foreword by John H. Conway.

[Pottier, 1996] Pottier, F. (1996). Simplifying subtyping constraints. In International Conference on Functional Programming, pages 122–133. ACM Press.

[Regnier and Urzyczyn, 2001] Regnier, L. and Urzyczyn, P. (2001). Retractions of types with many atoms. Technical Report 29, IML Marseille. http://arxiv.org/abs/cs/0212005.

[Rehof, 1998] Rehof, J. (1998). The Complexity of Simple Subtyping Systems. PhD thesis, Department of Computer Science, University of Copenhagen.

[Severi and de Vries, 2005] Severi, P. and de Vries, F. J. (2005). Order structures for Böhm-like models. In Computer Science Logic, volume 3634 of Lecture Notes in Computer Science, pages 103–116. Springer-Verlag.

[Simpson, 1995] Simpson, A. (1995). Categorical completeness results for simply-typed $λ$ -calculus. In [Dezani-Ciancaglini and Plotkin, 1995], pages 414–427.

[Smullyan, 1985] Smullyan, R. (1985). To Mock a Mockingbird. Knopf.

[Sørensen, 1997] Sørensen, M. (1997). Normalization in $λ$ -Calculus and Type Theory. PhD thesis, Department of Computer Science, University of Copenhagen. Available as DIKU Rapport 97/27.

[Spławski and Urzyczyn, 1999] Spławski, Z. and Urzyczyn, P. (1999). Type ﬁxpoints: Iteration vs. recursion. In International Conference on Functional Programming, pages 102–113. ACM Press.

[Statman, 1983] Statman, R. (1983). $λ$ -deﬁnable functionals and $β η$ conversion. Archiv für Mathematische Logik und Grundlagenforschung, 23:21–26.

[Statman, 1986] Statman, R. (1986). On translating lambda terms into combinators. In Logic in Computer Science, pages 378–382. IEEE Computer Society Press.

[Statman, 1988a] Statman, R. (1988a). Combinators hereditarily of order one. Technical Report 88-32, Department of Mathematics, Carnegie Mellon University.

[Statman, 1988b] Statman, R. (1988b). Combinators hereditarily of order two. Technical Report 88-33, Department of Mathematics, Carnegie Mellon University.

[Statman, 1989] Statman, R. (1989). The word problem for Smullyan’s Lark combinator is decidable. Journal of Symbolic Computation, 7(2):103–112.

[Statman, 1993] Statman, R. (1993). Some examples of non-existent combinators. Theoretical Computer Science, 121:441–448.

[Statman, 1997] Statman, R. (1997). Effective reduction and conversion strategies for combinators. In Rewriting Techniques and Applications, volume 1232 of Lecture Notes in Computer Science, pages 299–307. Springer-Verlag.

[Statman, 2000] Statman, R. (2000). On the word problem for combinators. In Rewriting Techniques and Applications, volume 1833 of Lecture Notes in Computer Science, pages 203–213. Springer-Verlag.

[Stirling, 2009] Stirling, C. (2009). Decidability of higher-order matching. Logical Methods in Computer Science, 5(3).

[Su et al., 2002] Su, Z., Aiken, A., Niehren, J., Priesnitz, T., and Treinen, R. (2002). The ﬁrst-order theory of subtyping constraints. In Symposium on Principles of Programming Languages, pages 203–216. ACM Press.

[Tatsuta, 2008] Tatsuta, M. (2008). Types for hereditary permutators. In Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science, LICS 2008, 24-27 June 2008, Pittsburgh, PA, USA. http://nii.ac.jp/TechReports/07-010E.html .

[Trifonov and Smith, 1996] Trifonov, V. and Smith, S. (1996). Subtyping constrained types. In Static Analysis Symposium, volume 1145 of Lecture Notes in Computer Science, pages 349–365. Springer-Verlag.

[Trigg et al., 1994] Trigg, P., Hindley, J. R., and Bunder, M. W. (1994). Combinatory abstraction using B, B’ and friends. Theoretical Computer Science, 135:405–422.

[Urzyczyn, 1996] Urzyczyn, P. (1996). Positive recursive type assignment. Fundamenta Informaticae, 28(1-2):197–209.

[Urzyczyn, 1997] Urzyczyn, P. (1997). Type reconstruction in $Fω$ . Mathematical Structures in Computer Science, 7(4):329–358.

[Urzyczyn, 1999] Urzyczyn, P. (1999). The emptiness problem for intersection types. Journal of Symbolic Logic, 64(3):1195–1215. (Preliminary version in Proc. LICS 94).

[Urzyczyn, 2009] Urzyczyn, P. (2009). Inhabitation of low-rank intersection types. In Curien, P.-L., editor, Typed Lambda Calculi and Applications, volume 5608 of Lecture Notes in Computer Science, pages 356–370. Springer-Verlag.

[Wadsworth, 1976] Wadsworth, C. P. (1976). The relation between computational and denotational properties for Scott’s $D ∞$ -models of the lambda-calculus. SIAM Journal of Computing, 5(3):488–521.

[Wilken and Weiermann, 2012] Wilken, G. and Weiermann, A. (2012). Derivation lengths classiﬁcation of Gödel’s $T$ extending Howard’s assignment. Logical Methods in Computer Science, 8(1):44.