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).
The podcast Iowa Type Theory Commute is embedded on this page from an open RSS feed. All files, descriptions, artwork and other metadata from the RSS-feed is the property of the podcast owner and not affiliated with or validated by Podplay.