@article(B11,
 author       = {Steffen van Bakel},
 year         = {2011},
 title        = {{Strict Intersection Types for the Lambda Calculus}},
 journal      = {{ACM Computing Surveys}},
 volume       = {43},
 number       = {3},
 pages        = {20},
 doi          = {10.1145/1922649.1922657},
)
@book(B84,
 author       = {Henk Barendregt},
 year         = {1984},
 title        = {The Lambda Calculus: its Syntax and Semantics},
 edition      = {revised},
 publisher    = {North-Holland},
)
@article(barecoppdeza83,
 author       = {Henk Barendregt and Mario Coppo and Mariangiola Dezani-Ciancaglini},
 year         = {1983},
 title        = {{A Filter Lambda Model and the Completeness of Type Assignment}},
 journal      = {The Journal of Symbolic Logic},
 volume       = {48},
 number       = {4},
 pages        = {931--940},
 doi          = {10.2307/2273659},
)
@book(BDS13,
 author       = {Henk Barendregt and Wil Dekkers and Richard Statman},
 year         = {2013},
 title        = {Lambda Calculus with Types},
 series       = {Perspectives in logic},
 publisher    = {Cambridge University Press},
 doi          = {10.1017/CBO9781139032636},
)
@inproceedings(BD74,
 author       = {Corrado B{\"{o}}hm and Mariangiola Dezani{-}Ciancaglini},
 year         = {1974},
 title        = {{Combinatorial Problems, Combinator Equations and Normal Forms}},
 editor       = {Jacques Loeckx},
 booktitle    = {ICALP'74},
 series       = {LNCS},
 volume       = {14},
 publisher    = {Springer},
 pages        = {185--199},
 doi          = {10.1007/3-540-06841-4\_60},
)
@article(BDL92,
 author       = {Kim Bruce and Roberto Di Cosmo and Giuseppe Longo},
 year         = {1992},
 title        = {Provable isomorphisms of types},
 journal      = {Mathematical Structures in Computer Science},
 volume       = {2},
 number       = {2},
 pages        = {231--247},
 doi          = {10.1017/S0960129500001444},
)
@inproceedings(BL85,
 author       = {Kim Bruce and Giuseppe Longo},
 year         = {1985},
 title        = {{Provable Isomorphisms and Domain Equations in Models of Typed Languages}},
 editor       = {Robert Sedgewick},
 booktitle    = {STOC'85},
 publisher    = {ACM Press},
 pages        = {263 -- 272},
 doi          = {10.1145/22145.22175},
)
@inproceedings(CDMZ13,
 author       = {Mario Coppo and Mariangiola Dezani-Ciancaglini and Ines Margaria and Maddalena Zacchi},
 year         = {2013},
 title        = {{Towards Isomorphism of Intersection and Union Types}},
 editor       = {Stephane Graham-Lengrand and Luca Paolini},
 booktitle    = {ITRS'12},
 series       = {EPTCS},
 volume       = {121},
 pages        = {58 -- 80},
 doi          = {10.4204/EPTCS.121.5},
)
@inproceedings(CDMZ14,
 author       = {Mario Coppo and Mariangiola Dezani-Ciancaglini and Ines Margaria and Maddalena Zacchi},
 year         = {2014},
 title        = {Isomorphism of ``Functional" Intersection Types},
 editor       = {Ralph Matthes and Aleksy Schubert},
 booktitle    = {Types'13},
 volume       = {26},
 publisher    = {LIPIcs},
 pages        = {129--149},
 doi          = {10.4230/LIPIcs.TYPES.2013.129},
)
@article(CDMZ16,
 author       = {Mario Coppo and Mariangiola Dezani-Ciancaglini and Ines Margaria and Maddalena Zacchi},
 year         = {2015},
 title        = {{Isomorphism of Intersection and Union Types}},
 journal      = {Mathematical Structures in Computer Science},
 doi          = {10.1017/S0960129515000304},
 note         = {Published online: 07 August 2015},
)
@inproceedings(CDMZ15,
 author       = {Mario Coppo and Mariangiola Dezani-Ciancaglini and Ines Margaria and Maddalena Zacchi},
 year         = {2015},
 title        = {{On Isomorphism of ``Functional'' Intersection and Union Types}},
 editor       = {Jacob Rehof},
 booktitle    = {ITRS'14},
 series       = {EPTCS},
 volume       = {177},
 pages        = {53--64},
 doi          = {10.4204/EPTCS.177},
)
@book(currfeys58,
 author       = {Haskell B. Curry and Robert Feys},
 year         = {1958},
 title        = {Combinatory Logic},
 series       = {Studies in Logic and the Foundations of Mathematics},
 volume       = {I},
 publisher    = {North-Holland},
)
@inproceedings(LPS92,
 author       = {Ugo de'Liguoro and Adolfo Piperno and Rick Statman},
 year         = {1992},
 title        = {{Retracts in Simply Typed $\lambda\beta \eta$-calculus}},
 editor       = {Andre Scedrov},
 booktitle    = {LICS'92},
 publisher    = {IEEE Computer Society Press},
 pages        = {461--469},
 doi          = {10.1109/LICS.1992.185557},
)
@article(DDGT10,
 author       = {Mariangiola Dezani-Ciancaglini and Roberto Di Cosmo and Elio Giovannetti and Makoto Tatsuta},
 year         = {2010},
 title        = {On Isomorphisms of Intersection Types},
 journal      = {ACM Transactions on Computational Logic},
 volume       = {11},
 number       = {4},
 pages        = {1--22},
 doi          = {10.1145/1805950.1805955},
)
@article(D95,
 author       = {Roberto Di Cosmo},
 year         = {1995},
 title        = {{Second Order Isomorphic Types. A Proof Theoretic Study on Second Order $\lambda$-calculus with Surjective Pairing and Terminal Object}},
 journal      = {Information and Computation},
 volume       = {119},
 number       = {2},
 pages        = {176--201},
 doi          = {10.1006/inco.1995.1085},
)
@article(D05,
 author       = {Roberto Di Cosmo},
 year         = {2005},
 title        = {{A Short Survey of Isomorphisms of Types}},
 journal      = {Mathematical Structures in Computer Science},
 volume       = {15},
 pages        = {825--838},
 doi          = {10.1017/S0960129505004871},
)
@article(FDB06,
 author       = {Marcelo Fiore and Roberto Di Cosmo and Vincent Balat},
 year         = {2006},
 title        = {{Remarks on Isomorphisms in Typed Lambda Calculi with Empty and Sum Types}},
 journal      = {Annals of Pure and Applied Logic},
 volume       = {141},
 number       = {1--2},
 pages        = {35--50},
 doi          = {10.1016/j.apal.2005.09.001},
)
@article(HL80,
 author       = {Roger Hindley and Giuseppe Longo},
 year         = {1980},
 title        = {Lambda-Calculus Models and Extensionality},
 journal      = {Mathematical Logic Quarterly},
 volume       = {26},
 number       = {19-21},
 pages        = {289--310},
 doi          = {10.1002/malq.19800261902},
)
@article(MZ83,
 author       = {Ines Margaria and Maddalena Zacchi},
 year         = {1983},
 title        = {{Right and Left Invertibility in Lambda-Beta-Calculus}},
 journal      = {R.A.I.R.O. Theoretical Informatics},
 volume       = {17},
 number       = {1},
 pages        = {71--88},
)
@inproceedings(P01,
 author       = {Vincent Padovani},
 year         = {2001},
 title        = {{Retracts in Simple Types}},
 editor       = {Samson Abramsky},
 booktitle    = {TLCA'01},
 series       = {LNCS},
 volume       = {2044},
 publisher    = {Springer},
 pages        = {376--384},
 doi          = {10.1007/3-540-45413-6\_29},
)
@article(RU02,
 author       = {Laurent Regnier and Pawel Urzyczyn},
 year         = {2002},
 title        = {{Retractions of Types with Many Atoms}},
 journal      = {CoRR},
 volume       = {cs.LO/0212005},
)
@article(S08,
 author       = {Aleksy Schubert},
 year         = {2008},
 title        = {{On the Building of Affine Retractions}},
 journal      = {Mathematical Structures in Computer Science},
 volume       = {18},
 number       = {4},
 pages        = {753--793},
 doi          = {10.1017/S096012950800683X},
)
@article(S83,
 author       = {Sergei Soloviev},
 year         = {1983},
 title        = {{The Category of Finite Sets and Cartesian Closed Categories}},
 journal      = {Journal of Soviet Mathematics},
 volume       = {22},
 number       = {3},
 pages        = {1387--1400},
 doi          = {10.1007/BF01084396},
 note         = {English translation of the original paper in Russian published in Zapiski Nauchnykh Seminarov LOMI, v.105, 1981},
)
@inproceedings(S93,
 author       = {Sergei Soloviev},
 year         = {1993},
 title        = {{A Complete Axiom System for Isomorphism of Types in Closed Categories}},
 editor       = {Andrei Voronkov},
 booktitle    = {LPAR'93},
 series       = {LNCS},
 volume       = {698},
 publisher    = {Springer},
 pages        = {360--371},
 doi          = {10.1007/3-540-56944-8\_71},
)
@inproceedings(SU99,
 author       = {Zdzislaw Splawski and Pawel Urzyczyn},
 year         = {1999},
 title        = {{Type Fixpoints: Iteration vs. Recursion}},
 editor       = {Didier R{\'{e}}mi and Peter Lee},
 booktitle    = {ICFP '99},
 publisher    = {ACM Press},
 pages        = {102--113},
 doi          = {10.1145/317636.317789},
)
@inproceedings(S13,
 author       = {Colin Stirling},
 year         = {2013},
 title        = {Proof Systems for Retracts in Simply Typed Lambda Calculus},
 editor       = {Fedor V. Fomin and Rusins Freivalds and Marta Z. Kwiatkowska and David Peleg},
 booktitle    = {ICALP'13},
 series       = {LNCS},
 volume       = {7966},
 publisher    = {Springer},
 pages        = {398--409},
 doi          = {10.1007/978-3-642-39212-2\_36},
)
@article(U99,
 author       = {Pawel Urzyczyn},
 year         = {1999},
 title        = {{The Emptiness Problem for Intersection Types}},
 journal      = {The Journal of Symbolic Logic},
 volume       = {64},
 number       = {3},
 pages        = {1195--1215},
 doi          = {10.2307/2586625},
)
@inproceedings(U09,
 author       = {Pawel Urzyczyn},
 year         = {2009},
 title        = {{Inhabitation of Low-Rank Intersection Types}},
 editor       = {Pierre{-}Louis Curien},
 booktitle    = {TLCA},
 series       = {LNCS},
 volume       = {5608},
 publisher    = {Springer},
 pages        = {356--370},
 doi          = {10.1007/978-3-642-02273-9\_26},
)