Intersection Types Preserved Under Beta-Expansion


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

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

128 つのエピソード