@inproceedings(Abel2007,
 author       = "Andreas Abel",
 year         = "2007",
 title        = "Syntactical strong normalization for intersection types with term rewriting rules",
 booktitle    = "Proceedings of HOR'07",
 pages        = "5--12",
)
@article(vanBakel92,
 author       = "Steffen van Bakel",
 year         = "1992",
 title        = "Complete restrictions of the intersection type discipline",
 journal      = "Theoretical Computer Science",
 volume       = "102",
 pages        = "135--163",
 doi          = "10.1016/0304-3975(92)90297-S",
)
@article(vanbakel04strongly,
 author       = "Steffen van Bakel",
 year         = "2004",
 title        = "Cut-elimination in the strict intersection type assignment system is strongly normalizing",
 journal      = "Notre Dame Journal of Formal Logic",
 volume       = "45",
 pages        = "35--63",
 doi          = "10.1305/ndjfl/1094155278",
)
@book(Barendregt2013,
 author       = "Henk Barendregt and Wil Dekkers and Richard Statman",
 year         = "2013",
 title        = "Lambda Calculus with Types",
 publisher    = "Cambridge University Press",
 doi          = "10.1017/CBO9781139032636",
)
@book(Barendregt1984,
 author       = "Henk P. Barendregt",
 year         = "1984",
 title        = "The Lambda Calculus: Its Syntax and Semantics",
 edition      = "revised",
 publisher    = "North-Holland",
 address      = "Amsterdam",
)
@inproceedings(Boudol2003,
 author       = "Gerard Boudol",
 year         = "2003",
 title        = "On strong normalization in the intersection type discipline",
 booktitle    = "Proceedings of TLCA'03",
 series       = "Lecture Notes in Computer Science 2701",
 publisher    = "Springer-Verlag",
 pages        = "60--74",
 doi          = "10.1007/3-540-44904-3\_5",
)
@article(BucciarelliPipernoSalvo2003,
 author       = "Antonio Bucciarelli and Adolfo Piperno and Ivano Salvo",
 year         = "2003",
 title        = "Intersection types and $\lambda $-definability",
 journal      = "Mathematical Structures in Computer Science",
 volume       = "13",
 pages        = "15--53",
 doi          = "10.1017/S0960129502003833",
)
@article(CDV1981,
 author       = "Mario Coppo and Mariangiola Dezani{-}Ciancaglini and Betti Venneri",
 year         = "1981",
 title        = "Functional characters of solvable terms",
 journal      = "Zeitschrift f\"ur Mathematische Logik und Grundlagen der Mathematik",
 volume       = "27",
 pages        = "45--58",
 doi          = "10.1002/malq.19810270205",
)
@article(David2001,
 author       = "Ren{\'e} David",
 year         = "2001",
 title        = "Normalization without reducibility",
 journal      = "Annals of Pure and Applied Logic",
 volume       = "107",
 pages        = "121--130",
 doi          = "10.1016/S0168-0072(00)00030-0",
)
@incollection(MR2001e:03033,
 author       = "Mariangiola Dezani-Ciancaglini and Elio Giovannetti and Ugo de'Liguoro",
 year         = "1998",
 title        = "Intersection types, {$\lambda $}-models, and {B}\"ohm trees",
 booktitle    = "Theories of Types and Proofs",
 series       = "MSJ Memoirs",
 volume       = "2",
 publisher    = "Mathematical Society of Japan",
 address      = "Tokyo",
 pages        = "45--97",
)
@article(MR2003d:03016,
 author       = "Mariangiola Dezani-Ciancaglini and Furio Honsell and Yoko Motohama",
 year         = "2001",
 title        = "Approximation theorems for intersection type systems",
 journal      = "Journal of Logic and Computation",
 volume       = "11",
 pages        = "395--417",
 doi          = "10.1093/logcom/11.3.395",
)
@article(JoachimskiMatthes2003,
 author       = "Felix Joachimski and Ralph Matthes",
 year         = "2003",
 title        = "Short proofs of normalization for the simply-typed $\lambda $-calculus, permutative conversions and {G\"{o}del's} {T}",
 journal      = "Archive for Mathematical Logic",
 volume       = "42",
 pages        = "59--87",
 doi          = "10.1007/s00153-002-0156-9",
)
@article(KamareddineRW12,
 author       = "Fairouz Kamareddine and Vincent Rahli and Joe B. Wells",
 year         = "2012",
 title        = "Reducibility proofs in the $\lambda $-calculus",
 journal      = "Fundamenta Informaticae",
 volume       = "121",
 pages        = "121--152",
 doi          = "10.3233/FI-2012-773",
)
@inproceedings(KfouryWells1995,
 author       = "Assaf J. Kfoury and Joe B. Wells",
 year         = "1995",
 title        = "New notions of reduction and non-semantic proofs of strong $\beta $-normalization in typed $\lambda $-calculi",
 booktitle    = "Proceedings of LICS'95",
 publisher    = "IEEE Computer Society Press",
 pages        = "311--321",
 doi          = "10.1109/LICS.1995.523266",
)
@inproceedings(Kikuchi2009,
 author       = "Kentaro Kikuchi",
 year         = "2009",
 title        = "On general methods for proving reduction properties of typed lambda terms",
 booktitle    = "Proof theoretical study of the structure of logic and computation",
 series       = "RIMS K\^oky\^uroku 1635",
 pages        = "33--50",
 url          = "http://hdl.handle.net/2433/140464",
 note         = "(Unrefereed proceedings)",
)
@inproceedings(Matthes2000,
 author       = "Ralph Matthes",
 year         = "2000",
 title        = "Characterizing strongly normalizing terms of a {$\lambda $}-calculus with generalized applications via intersection types",
 booktitle    = "Proceedings of ICALP Satellite Workshops 2000",
 publisher    = "Carleton Scientific",
 pages        = "339--354",
)
@incollection(Pottinger1980,
 author       = "Garrel Pottinger",
 year         = "1980",
 title        = "A type assignment for the strongly normalizable {$\lambda $}-terms",
 booktitle    = "To H.~B.~Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism",
 publisher    = "Academic Press",
 address      = "London",
 pages        = "561--577",
)
@techreport(vRS1995,
 author       = "Femke van Raamsdonk and Paula Severi",
 year         = "1995",
 title        = "On normalisation",
 type         = "Technical Report",
 number       = "CS-R9545",
 institution  = "CWI",
)
@article(vRSSX1999,
 author       = "Femke van Raamsdonk and Paula Severi and Morten Heine B. S{\o }rensen and Hongwei Xi",
 year         = "1999",
 title        = "Perpetual reductions in {$\lambda $}-calculus",
 journal      = "Information and Computation",
 volume       = "149",
 pages        = "173--225",
 doi          = "10.1006/inco.1998.2750",
)
@article(Tait1967,
 author       = "William W. Tait",
 year         = "1967",
 title        = "Intensional interpretations of functionals of finite type {I}",
 journal      = "The Journal of Symbolic Logic",
 volume       = "32",
 pages        = "198--212",
 doi          = "10.2307/2271658",
)
@article(Valentini2001,
 author       = "Silvio Valentini",
 year         = "2001",
 title        = "An elementary proof of strong normalization for intersection types",
 journal      = "Archive for Mathematical Logic",
 volume       = "40",
 pages        = "475--488",
 doi          = "10.1007/s001530000070",
)