Steffen van Bakel (2011):
Strict Intersection Types for the Lambda Calculus.
ACM Computing Surveys 43(3),
pp. 20,
doi:10.1145/1922649.1922657.
Henk Barendregt (1984):
The Lambda Calculus: its Syntax and Semantics,
revised edition.
North-Holland.
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.
Henk Barendregt, Wil Dekkers & Richard Statman (2013):
Lambda Calculus with Types.
Perspectives in logic.
Cambridge University Press,
doi:10.1017/CBO9781139032636.
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.
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.
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.
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.
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.
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.
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.
Haskell B. Curry & Robert Feys (1958):
Combinatory Logic.
Studies in Logic and the Foundations of Mathematics I.
North-Holland.
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.
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.
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.
Roberto Di Cosmo (2005):
A Short Survey of Isomorphisms of Types.
Mathematical Structures in Computer Science 15,
pp. 825–838,
doi:10.1017/S0960129505004871.
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.
Roger Hindley & Giuseppe Longo (1980):
Lambda-Calculus Models and Extensionality.
Mathematical Logic Quarterly 26(19-21),
pp. 289–310,
doi:10.1002/malq.19800261902.
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.
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.
Laurent Regnier & Pawel Urzyczyn (2002):
Retractions of Types with Many Atoms.
CoRR cs.LO/0212005.
Aleksy Schubert (2008):
On the Building of Affine Retractions.
Mathematical Structures in Computer Science 18(4),
pp. 753–793,
doi:10.1017/S096012950800683X.
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.
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.
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.
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.
Pawel Urzyczyn (1999):
The Emptiness Problem for Intersection Types.
The Journal of Symbolic Logic 64(3),
pp. 1195–1215,
doi:10.2307/2586625.
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.
eptcs@eptcs.org