Retractions in Intersection Types
Logic in Computer Science
2017-02-09 v1
Abstract
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.
Cite
@article{arxiv.1702.02274,
title = {Retractions in Intersection Types},
author = {Mario Coppo and Mariangiola Dezani-Ciancaglini and Alejandro Díaz-Caro and Ines Margaria and Maddalena Zacchi},
journal= {arXiv preprint arXiv:1702.02274},
year = {2017}
}
Comments
In Proceedings ITRS 2016, arXiv:1702.01874