Normal terms are typable with intersection types

Iowa Type Theory Commute
05/03/2021 10 min Temporada 2 Episodio 22
Normal terms are typable with intersection types

Listen "Normal terms are typable with intersection types"

Descargar episodio

Episode Synopsis

I sketch the argument that pure lambda terms in normal form are typable using intersection types.  This completes the argument started in the previous episode, that intersection types are complete for normalizing terms: normal forms are typable, and typing is preserved by beta-expansion.  Hence any normalizing term is typable (since it reduces to a normal form by definition, and from this normal form we can walk typing back to the term).
© 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