Thumbnail
Access Restriction
Subscribed

Author Bakel, Steffen Van
Source ACM Digital Library
Content type Text
Publisher Association for Computing Machinery (ACM)
File Format PDF
Copyright Year ©2011
Language English
Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science
Subject Keyword λ-calculus ♦ Strict intersection types ♦ Approximation ♦ Filter semantics ♦ Normalization ♦ Principal pairs
Abstract 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.
ISSN 03600300
Age Range 18 to 22 years ♦ above 22 year
Educational Use Research
Education Level UG and PG
Learning Resource Type Article
Publisher Date 2011-04-01
Publisher Place New York
e-ISSN 15577341
Journal ACM Computing Surveys (CSUR)
Volume Number 43
Issue Number 3
Page Count 49
Starting Page 1
Ending Page 49


Open content in new tab

   Open content in new tab
Source: ACM Digital Library