Uniqueness typing for intersection types

2021/05/05 by Richard Statman, Statman, Richard, Andrew Polonsky +1
Computer Science · Engineering · Mathematics · #03B38 #F.4.1 #FOS: Computer and information sciences #FOS: Mathematics #Formal Methods in Verification #Logic (math.LO) #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #acm:03B38 #cs.LO #graph theory and CDMA systems #math.LO #msc:03B38

paper · pdf · doi:10.48550/arxiv.2105.02352

Superseded by arXiv:1809.08169v2

openalex publication_date 2021/05/05 · arxiv created 2021/05/09 · arxiv updated 2021/05/11 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

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 (Γ,A) such that 1) Γ\vdash M : A 2) Γ\vdash N : A \Longrightarrow M =_βη N We also discuss several presentations of intersection type algebras, and the corresponding choices of type assignment rules.

Related

• Strong normalization through idempotent intersection types: a new syntactical approach
• Structural Rules and Algebraic Properties of Intersection Types
• A complete realisability semantics for intersection types and arbitrary expansion variables
• Intersection Types via Finite-Set Declarations
• Sound and Complete Bidirectional Typechecking for Higher-Rank Polymorphism with Existentials and Indexed Types