Research on "Semantics and Logics of Computation"

Intersection Types and Lambda Definability

ABSTRACT. This paper presents a novel method to compare computational properties of $\lambda$-terms typeable with intersection types, with respect to terms typeable with Curry types. We introduce a translation from intersection typing {\em derivations} to Curry typeable {\em terms} which 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 proves strong normalization for the intersection system naturally by means of purely syntactical techniques. The paper extends the results presented in [Bucciarelli, De Lorenzis, Piperno, Salvo, Some Computational Properties of Intersection Types , LICS'99] to the whole intersection type system of Barendregt, Coppo and Dezani, thus providing a complete proof of a conjecture proposed by Leivant in 1990: all functions uniformly definable using intersection types are already definable using Curry types.

• pdf ( © Cambridge University Press )

BIBTEX.

@article{Bucciarelli-Piperno-Salvo:MSCS-0X,
   author    = {A. Bucciarelli and A. Piperno and I. Salvo},
   title     = {Intersection Types and Lambda Definability},
   journal   = {Mathematical Structures in Computer Science},
   year      = {To appear},
   volume    = {200X},
   number    = {},
   pages     = {},
   publisher = {Cambridge University Press},
}