-
- Steffen Van Bakel
- Imperial College London, London, U.K.
書誌事項
- 公開日
- 2011-04
- 権利情報
-
- https://www.acm.org/publications/policies/copyright_policy#Background
- DOI
-
- 10.1145/1922649.1922657
- 公開者
- Association for Computing Machinery (ACM)
この論文をさがす
説明
<jats:p>This article will show the usefulness and elegance of strict intersection types for the Lambda Calculus, that are strict in the sense that they are the representatives of equivalence classes of types in the BCD-system [Barendregt et al. 1983]. We will focus on the essential intersection type assignment; this system is almost syntax directed, and we will show that all major properties hold that are known to hold for other intersection systems, like the approximation theorem, the characterization of (head/strong) normalization, completeness of type assignment using filter semantics, strong normalization for cut-elimination and the principal pair property. In part, the proofs for these properties are new; we will briefly compare the essential system with other existing systems.</jats:p>
収録刊行物
-
- ACM Computing Surveys
-
ACM Computing Surveys 43 (3), 1-49, 2011-04
Association for Computing Machinery (ACM)
