Advanced Properties and Applications
This chapter proves some properties of intersection types in relation to terms and models.
Section 17.1 defines a realizability interpretation of types (Barendregt et al. (1983)). Types are interpreted as subsets of a domain of discourse D. Assuming a (partial) application , and a type environment ξ, i.e. a mapping from type atoms to subsets of D, we can define an interpretation for each type A in by giving ...