Franco Barbanera, Mariangiola Dezani-Ciancaglini & Ugo de'Liguoro (1995):
Intersection and Union Types: Syntax and Semantics.
Information and Computation 119(2),
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: Robert Sedgewick: STOC'85.
ACM Press,
pp. 263 – 272,
doi:10.1145/22145.22175.
Mario Coppo, Mariangiola Dezani-Ciancaglini, Ines Margaria & Maddalena Zacchi (2013):
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 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.
Donald Knuth & Peter Bendix (1970):
Simple word problems in universal algebras.
In: J. Leech: Computational Problems in Abstract Algebra.
Pergamon Press,
pp. 263–297.
David MacQueen, Gordon Plotkin & Ravi Sethi (1986):
An Ideal Model for Recursive Polymorphic Types.
Information and Control 71(1-2),
pp. 95–130,
doi:10.1016/S0019-9958(86)80019-5.
Dag Prawitz (1965):
Natural Deduction.
Almqvist & Wiksell.
Richard Routley & Robert K. Meyer (1972):
The Semantics of Entailment III.
Journal of Philosophical Logic 1(2),
pp. 192–208,
doi:10.1007/BF00650498.
Sergei Soloviev (1993):
A Complete Axiom System for Isomorphism of Types in Closed Categories.
In: A. Voronkov: LPAR'93,
Lecture Notes in Computer Science 698.
Springer-Verlag,
pp. 360–371,
doi:10.1007/3-540-56944-8_71.
Sergei V. 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.