Logic in Computer Science (LICS 1999)

Paper: Some Computational Properties of Intersection Types (at LICS 1999)

Authors: Antonio Bucciarelli Silvia de Lorenzis Adolfo Piperno Ivano Salvo

Abstract

This paper presents a new method for comparing computational properties of \math-terms typeable with intersection types with respect to terms typeable with Curry types. In particular, strong normalization and \math-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.

BibTeX

  @InProceedings{BucciarelliLorenzis-SomeComputationalPr,
    author = 	 {Antonio Bucciarelli and Silvia de Lorenzis and Adolfo Piperno and Ivano Salvo},
    title = 	 {Some Computational Properties of Intersection Types},
    booktitle =  {Proceedings of the Fourteenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1999},
    year =	 1999,
    editor =	 {Giuseppe Longo},
    month =	 {July}, 
    pages =      {109--118},
    location =   {Trento, Italy}, 
    publisher =	 {IEEE Computer Society Press}
  }