Retractions in Intersection Types

Mario Coppo
(Università di Torino)
Mariangiola Dezani-Ciancaglini
(Università di Torino)
Alejandro Díaz-Caro
(CONICET & Universidad Nacional de Quilmes)
Ines Margaria
(Università di Torino)
Maddalena Zacchi
(Università di Torino)

This paper deals with retraction - intended as isomorphic embedding - in intersection types building left and right inverses as terms of a lambda calculus with a bottom constant. The main result is a necessary and sufficient condition two strict intersection types must satisfy in order to assure the existence of two terms showing the first type to be a retract of the second one. Moreover, the characterisation of retraction in the standard intersection types is discussed.

In Naoki Kobayashi: Proceedings Eighth Workshop on Intersection Types and Related Systems (ITRS 2016), Polto, Portugal, 26th June 2016, Electronic Proceedings in Theoretical Computer Science 242, pp. 31–47.
Published: 7th February 2017.

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