Social networks and discovery in the enterprise (SaND)
Inbal Ronen, Elad Shahar, et al.
SIGIR 2009
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.
Inbal Ronen, Elad Shahar, et al.
SIGIR 2009
Leo Liberti, James Ostrowski
Journal of Global Optimization
Thomas M. Cheng
IT Professional
Qing Li, Zhigang Deng, et al.
IEEE T-MI