PT Journal
AU Bucciarelli, A
   de Lorenzis, S
   Piperno, A
   Salvo, I
TI Some Computational Properties of Intersection Types (Extended Abstract)
PY 1999
BP 109
EP 118
DI 10.1109/LICS.1999.782598
DE lambda calculusCurry types; intersection types; lambda-definability; lambda-terms; strong normalization
AB This paper presents a new method for comparing computation-properties of λ-terms typeable with intersection types with respect to terms typeable with Curry types. In particular, strong normalization and λ-definability are investigated. A translation is introduced from intersection typing derivations to Curry typeable terms; the main feature of the proposed technique is that the translation is preserved by β-reduction. This allows to simulate a computation starting from a term typeable in the intersection discipline by means of a computation starting from a simply typeable term. Our approach naturally leads to prove strong normalization in the intersection system by means of purely syntactical techniques. In addition, the presented method enables us to give a proof of a conjecture proposed by Leivant in 1990, namely that all functions uniformly definable using intersection types are already definable using Curry types.
ER