Podcasts Technology Iowa Type Theory Commute Normal terms are typable with intersection types

Normal terms are typable with intersection types

Published: March 5, 2021, 6 a.m.

b'

I sketch the argument that pure lambda terms in normal form are typable using intersection types.\\xa0 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.\\xa0 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).

'