Toward Isomorphism of Intersection and Union types

Mario Coppo
(Universita' di Torino)
Mariangiola Dezani-Ciancaglini
(Universita' di Torino)
Ines Margaria
(Universita' di Torino)
Maddalena Zacchi
(Universita' di Torino)

This paper investigates type isomorphism in a lambda-calculus with intersection and union types. It is known that in lambda-calculus, the isomorphism between two types is realised by a pair of terms inverse one each other. Notably, invertible terms are linear terms of a particular shape, called finite hereditary permutators. Typing properties of finite hereditary permutators are then studied in a relevant type inference system with intersection and union types for linear terms. In particular, an isomorphism preserving reduction between types is defined. Type reduction is confluent and terminating, and induces a notion of normal form of types. The properties of normal types are a crucial step toward the complete characterisation of type isomorphism. The main results of this paper are, on one hand, the fact that two types with the same normal form are isomorphic, on the other hand, the characterisation of the isomorphism between types in normal form, modulo isomorphism of arrow types.

In Stéphane Graham-Lengrand and Luca Paolini: Proceedings Sixth Workshop on Intersection Types and Related Systems (ITRS 2012), Dubrovnik, Croatia, 29th June 2012, Electronic Proceedings in Theoretical Computer Science 121, pp. 58–80.
Published: 30th July 2013.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: