Podcasts Technology Iowa Type Theory Commute Intersection Types Preserved Under Beta-Expansion

Intersection Types Preserved Under Beta-Expansion

Published: Feb. 15, 2021, 6 a.m.

b'

Type systems usually have the type preservation property: if a typable term beta-reduces, then the resulting term is still typable.\\xa0 So typing is closed under beta-reduction.\\xa0 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).\\xa0\\xa0

'