Embedding a Second-Order Type System into an Intersection Type System

This paper presents the relationship between a second-order type assignment system T ∀ and an intersection type assignment system T ∧. First we define a translation tr from intersection types to second-order types. Then we define a system T ∧* obtained from T ∧ by restricting the use of the intersection type introduction rule, and show that T ∧* and T ∀ are equivalent in the following senses: (a) if a λ-term M has a type σ in T ∧*, then M has the type tr(σ) in T ∀; and conversely, (b) if M has a type T in T ∀, then M has a type σ in T ∧* such that tr(σ) is equivalent to T. These two theorems mean that T ∀ is embedded into T ∧.

Authors

• H. Yokouchi

Keywords

No keywords are indexed for this paper.