@Article{Bucciarelli_etal1999,
author="Bucciarelli, Antonio
and de Lorenzis, Silvia
and Piperno, Adolfo
and Salvo, Ivano",
title="Some Computational Properties of Intersection Types (Extended Abstract)",
year="1999",
publisher="IEEE Computer Society",
pages="109--118",
optkeywords="lambda calculusCurry types; intersection types; lambda-definability; lambda-terms; strong normalization",
abstract="This paper presents a new method for comparing computation-properties of $\lambda$-terms typeable with intersection types with respect to terms typeable with Curry types. In particular, strong normalization and $\lambda$-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 $\beta$-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.",
optnote="exported from refbase (http://mclab.di.uniroma1.it/publications/show.php?record=71), last updated on Thu, 22 Nov 2012 14:59:18 +0100",
doi="10.1109/LICS.1999.782598",
opturl="https://doi.org/10.1109/LICS.1999.782598",
file=":http://mclab.di.uniroma1.it/publications/papers/papers/Bucciarelli1999.pdf:PDF"
}