The study of type isomorphisms for different lambda-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 lambda-calculus. In particular, isomorphism is not a congruence and types that are equal in the standard models of intersection types may be non-isomorphic.
On Isomorphisms of Intersection Types
DEZANI, Mariangiola;GIOVANNETTI, Elio;
2010-01-01
Abstract
The study of type isomorphisms for different lambda-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 lambda-calculus. In particular, isomorphism is not a congruence and types that are equal in the standard models of intersection types may be non-isomorphic.File | Dimensione | Formato | |
---|---|---|---|
isomorphisms.pdf
Accesso riservato
Tipo di file:
POSTPRINT (VERSIONE FINALE DELL’AUTORE)
Dimensione
228.89 kB
Formato
Adobe PDF
|
228.89 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.