@article(barba,
 author       = "Franco Barbanera and Mariangiola Dezani-Ciancaglini and Ugo de'Liguoro",
 year         = "1995",
 title        = "Intersection and Union Types: Syntax and Semantics",
 journal      = "Information and Computation",
 volume       = "119",
 number       = "2",
 pages        = "202--230",
 doi          = "10.1006/inco.1995.1086",
)
@article(BruceDicosmoLongo92,
 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(BruceLongo85,
 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",
)
@article(CDMZ13,
 author       = "Mario Coppo and Mariangiola Dezani-Ciancaglini and Ines Margaria and Maddalena Zacchi",
 year         = "2013",
 title        = "Isomorphism of Intersection and Union Types",
 journal      = "Mathematical Structures in Computer Science",
 note         = "To appear",
)
@article(D82,
 author       = "Nachum Dershowitz",
 year         = "1982",
 title        = "Orderings for term-rewriting systems",
 journal      = "Theoretical Computer Science",
 volume       = "17",
 number       = "3",
 pages        = "279 -- 301",
 doi          = "10.1016/0304-3975(82)90026-3",
)
@article(Dezani,
 author       = "Mariangiola {Dezani-Ciancaglini}",
 year         = "1976",
 title        = "Characterization of Normal Forms Possessing an Inverse in the {$\lambda \beta \eta $}-calculus",
 journal      = "Theoretical Computer Science",
 volume       = "2",
 number       = "3",
 pages        = "323--337",
 doi          = "10.1016/0304-3975(76)90085-2",
)
@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(Dicosmo93,
 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(MSCSSurvey05,
 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",
)
@inproceedings(KB70,
 author       = "Donald Knuth and Peter Bendix",
 year         = "1970",
 title        = "Simple word problems in universal algebras",
 editor       = "J. Leech",
 booktitle    = "Computational Problems in Abstract Algebra",
 publisher    = "Pergamon Press",
 pages        = "263--297",
)
@article(MQPS86,
 author       = "David MacQueen and Gordon Plotkin and Ravi Sethi",
 year         = "1986",
 title        = "An Ideal Model for Recursive Polymorphic Types",
 journal      = "Information and Control",
 volume       = "71",
 number       = "1-2",
 pages        = "95--130",
 doi          = "10.1016/S0019-9958(86)80019-5",
)
@book(praw65,
 author       = "Dag Prawitz",
 year         = "1965",
 title        = "Natural Deduction",
 publisher    = "Almqvist \&\ Wiksell",
)
@article(SE3,
 author       = "Richard Routley and Robert K. Meyer",
 year         = "1972",
 title        = "The Semantics of Entailment {III}",
 journal      = "Journal of Philosophical Logic",
 volume       = "1",
 number       = "2",
 pages        = "192--208",
 doi          = "10.1007/BF00650498",
)
@inproceedings(soloviev93complete,
 author       = "Sergei Soloviev",
 year         = "1993",
 title        = "A Complete Axiom System for Isomorphism of Types in Closed Categories",
 editor       = "A. Voronkov",
 booktitle    = "LPAR'93",
 series       = "Lecture Notes in Computer Science",
 volume       = "698",
 publisher    = "Springer-Verlag",
 pages        = "360--371",
 doi          = "10.1007/3-540-56944-8\_71",
)
@article(Solovev83,
 author       = "Sergei V. 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",
)