Retractions in Intersection Types

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.

In Proceedings ITRS 2016, arXiv:1702.01874

References in corpus (3)

• Retractions of Types with Many Atoms
• On Isomorphism of "Functional" Intersection and Union Types
• Proceedings Seventh Workshop on Intersection Types and Related Systems