Intersection Types Preserved Under Beta-Expansion

Iowa Type Theory Commute
15/02/2021 12 min Temporada 2 Episodio 21
Intersection Types Preserved Under Beta-Expansion

Listen "Intersection Types Preserved Under Beta-Expansion"

Descargar episodio

Episode Synopsis

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).  
© 2003-2025 ZARZA | AHEAD OF OUR TIME
privacy policy
In God we trust In God we trust
PreSales Questions? Click Here
or call our toll-free line at +1-888-5002068 Miami, Florida, USA