Intersection Types Preserved Under Beta-Expansion

Iowa Type Theory Commute

English - February 15, 2021 06:00 - 12 minutes - 8.43 MB - ★★★★★ - 13 ratings
Technology Science Mathematics programming languages computational logic type theory proof assistants cedille Homepage Download Apple Podcasts Google Podcasts Overcast Castro Pocket Casts RSS feed

Previous Episode: Introduction to Intersection Types

Next Episode: Normal terms are typable with intersection types

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).