Performance measurement and data base design
Alfonso P. Cardenas, Larry F. Bowman, et al.
ACM Annual Conference 1975
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∧. © 1995 Academic Press, Inc.
Alfonso P. Cardenas, Larry F. Bowman, et al.
ACM Annual Conference 1975
Preeti Malakar, Thomas George, et al.
SC 2012
Khaled A.S. Abdel-Ghaffar
IEEE Trans. Inf. Theory
György E. Révész
Theoretical Computer Science