On isomorphisms of intersection types

The study of type isomorphisms for different λ-calculi started over twenty years ago, and a very wide body of knowledge has been established, both in terms of results and in terms of techniques. A notable missing piece of the puzzle was the characterization of type isomorphisms in the presence of in...

Full description

Saved in:
Bibliographic Details
Published in:ACM transactions on computational logic 2010-07, Vol.11 (4), p.1-24
Main Authors: Dezani-Ciancaglini, Mariangiola, Cosmo, Roberto Di, Giovannetti, Elio, Tatsuta, Makoto
Format: Article
Language:English
Subjects:
Computer Science
Programming Languages
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:The study of type isomorphisms for different λ-calculi started over twenty years ago, and a very wide body of knowledge has been established, both in terms of results and in terms of techniques. A notable missing piece of the puzzle was the characterization of type isomorphisms in the presence of intersection types. While, at first thought, this may seem to be a simple exercise, it turns out that not only finding the right characterization is not simple, but that the very notion of isomorphism in intersection types is an unexpectedly original element in the previously known landscape, breaking most of the known properties of isomorphisms of the typed λ-calculus. In particular, isomorphism is not a congruence and types that are equal in the standard models of intersection types may be nonisomorphic.
ISSN:1529-3785
1557-945X
DOI:10.1145/1805950.1805955