TY  - JOUR
AU  - Bucciarelli, Antonio
AU  - de Lorenzis, Silvia
AU  - Piperno, Adolfo
AU  - Salvo, Ivano
PY  - 1999
DA  - 1999//
TI  - Some Computational Properties of Intersection Types (Extended Abstract)
SP  - 109
EP  - 118
PB  - IEEE Computer Society
KW  - lambda calculusCurry types
KW  - intersection types
KW  - lambda-definability
KW  - lambda-terms
KW  - 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.
L1  - http://mclab.di.uniroma1.it/publications/papers/papers/Bucciarelli1999.pdf
UR  - https://doi.org/10.1109/LICS.1999.782598
DO  - 10.1109/LICS.1999.782598
N1  - exported from refbase (http://mclab.di.uniroma1.it/publications/show.php?record=71), last updated on Thu, 22 Nov 2012 14:59:18 +0100
ID  - Bucciarelli_etal1999
ER  -