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

Comments and questions to:
For website issues: