期刊名称：Electronic Proceedings in Theoretical Computer Science
电子版ISSN：2075-2180
出版年度：2019
卷号：293
页码：29-37
DOI：10.4204/EPTCS.293.3
语种：English
出版社：Open Publishing Association
摘要：Refining and extending previous work by Retoré, we develop a systematic approach to intersection types via natural deduction. We show how a step of beta reduction can be seen as performing, at the level of typing derivations, Prawitz reductions in parallel. Then we derive as immediate consequences of Subject Reduction the main theorems about normalization for intersection types: for system D, strong normalization, for system Omega, the leftmost reduction termination for terms typable without Omega.
