Retractions in Intersection Types

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 t...

Full description

Bibliographic Details
Main Authors: Mario Coppo, Mariangiola Dezani-Ciancaglini, Alejandro Díaz-Caro, Ines Margaria, Maddalena Zacchi
Format: Article
Language:English
Published: Open Publishing Association 2017-02-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1702.02274v1