Uniqueness typing for intersection types
Logic in Computer Science
2021-05-11 v2 Logic
Abstract
Working in a variant of the intersection type assignment system of Coppo, Dezani-Ciancaglini and Veneri [1981], we prove several facts about sets of terms having a given intersection type. Our main result is that every strongly normalizing term admits a *uniqueness typing*, which is a pair such that 1) 2) We also discuss several presentations of intersection type algebras, and the corresponding choices of type assignment rules.
Keywords
Cite
@article{arxiv.2105.02352,
title = {Uniqueness typing for intersection types},
author = {Richard Statman and Andrew Polonsky},
journal= {arXiv preprint arXiv:2105.02352},
year = {2021}
}
Comments
Superseded by arXiv:1809.08169v2