Normal terms are typable with intersection types


Manage episode 286573147 series 2823367
著作 Aaron Stump の情報はPlayer FM及びコミュニティによって発見されました。著作権は出版社によって所持されます。そして、番組のオーディオは、その出版社のサーバから直接にストリーミングされます。Player FMで購読ボタンをタップし、更新できて、または他のポッドキャストアプリにフィードのURLを貼り付けます。

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

122 つのエピソード