Uniqueness typing for intersection types

MaRDI QIDQ6366940zbMATH OpenFDO

Authors Richard Statman, Andrew Polonsky

Publication date 5 May 2021

Mathematics Subject Classification ID

Type theory (03B38)

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 $M$ admits a *uniqueness typing*, which is a pair $(Gamma,A)$ such that 1) $GammavdashM:A$ 2) $$ We also discuss several presentations of intersection type algebras, and the corresponding choices of type assignment rules.

This page was built for publication: Uniqueness typing for intersection types

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6366940)