Franco Barbanera, Mariangiola Dezani-Ciancaglini & Ugo de'Liguoro (1995):
Intersection and Union Types: Syntax and Semantics.
Information and Computation 119,
pp. 202–230,
doi:10.1006/inco.1995.1086.
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: R. Sedgewick: STOC'85.
ACM Press,
pp. 263 – 272,
doi:10.1145/22145.22175.
Mario Coppo, Mariangiola Dezani-Ciancaglini, Furio Honsell & Giuseppe Longo (1984):
Extended Type Structures and Filter Lambda Models.
In: G. Lolli, G. Longo & A. Marcja: LC'82.
North-Holland,
pp. 241–262.
Mario Coppo, Mariangiola Dezani-Ciancaglini, Ines Margaria & Maddalena Zacchi (2013):
Towards Isomorphism of Intersection and Union Types.
In: S. Graham-Lengrand & L. 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 (2014):
Isomorphism of Intersection and Union Types.
Mathematical Structures in Computer Science.
To appear.
Nachum Dershowitz (1982):
Orderings for Term-Rewriting Systems.
Theoretical Computer Science 17(3),
pp. 279 – 301,
doi:10.1016/0304-3975(82)90026-3.
Mariangiola Dezani-Ciancaglini (1976):
Characterization of Normal Forms Possessing an Inverse in the λβη-Calculus.
Theoretical Computer Science 2(3),
pp. 323–337,
doi:10.1016/0304-3975(76)90085-2.
Mariangiola Dezani-Ciancaglini, Roberto Di Cosmo, Elio Giovannetti & Makoto Tatsuta (2010):
On Isomorphisms of Intersection Types.
ACM TOCL 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.
Alejandro Díaz-Caro & Gilles Dowek (2015):
Simply Typed Lambda-Calculus Modulo Type Isomorphisms.
Theoretical Computer Science.
To appear.
Neil Mitchell (2008):
Hoogle Overview.
The Monad.Reader 12,
pp. 27–35.
Maxwell H. A. Newman (1942):
On Theories with a Combinatorial Definition of ``Equivalence''.
Annals of Mathematics 43(2),
pp. 223–243,
doi:10.2307/1968867.
Richard Routley & Robert K. Meyer (1972):
The Semantics of Entailment III.
Journal of Philosophical Logic 1,
pp. 192–208,
doi:10.1007/BF00650498.
Dana Scott (1972):
Continuous Lattices.
In: F. W. Lawvere: Toposes, Algebraic Geometry, and Logic,
LNM 274.
Springer-Verlag,
pp. 97–136,
doi:10.1007/BFb0073967.
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 Nauchnych Seminarov LOMI, v.105, 1981.
Sergei Soloviev (1993):
A Complete Axiom System for Isomorphism of Types in Closed Categories.
In: A. Voronkov: LPAR'93,
LNCS 698.
Springer-Verlag,
pp. 360–371,
doi:10.1007/3-540-56944-8_71.