Start / Iowa Type Theory Commute / Intersection types preserved under beta expansion

Intersection Types Preserved Under Beta-Expansion

12 min • 15 februari 2021

Type systems usually have the type preservation property: if a typable term beta-reduces, then the resulting term is still typable. So typing is closed under beta-reduction. With intersection typing, typing is also closed under beta-expansion, which is a critical step in showing that intersection typing is complete for normalizing terms: any normalizing term can be typed with intersection types (and simple function types).