Research on "Semantics and Logics of Computation"

Some Computational Properties of Intersection Types (Extended Abstract)

ABSTRACT. This paper presents a new method for comparing computational 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.

BIBTEX.

@conference{bucciarelli-delorenzis-piperno-salvo:99,
   author    = {A. Bucciarelli and S. de Lorenzis and A. Piperno and I. Salvo},
   title     = {Some Computational Properties of Intersection Types (Extended Abstract)},
   booktitle = {{Proceedings of 14th LICS}},
   year      = {1999},
   publisher = {IEEE Computer Society},
   pages     = {109--118},
   series    = {LNCS},
}