toggle visibility Search & Display Options

Select All    Deselect All
 |   | 
Details
   print
  Record Links
Author Bucciarelli, Antonio; Piperno, Adolfo; Salvo, Ivano file  doi
openurl 
  Title Intersection types and λ-definability Type Journal Article
  Year 2003 Publication Mathematical Structures in Computer Science Abbreviated Journal  
  Volume 13 Issue 1 Pages 15-53  
  Keywords  
  Abstract This paper presents a novel method for comparing computational properties of λ-terms that are typeable with intersection types, with respect to terms that are typeable with Curry types. We introduce a translation from intersection typing derivations to Curry typeable terms that is preserved by β-reduction: this allows the simulation of 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 normalisation for the intersection system naturally by means of purely syntactical techniques. The paper extends the results presented in Bucciarelli et al. (1999) to the whole intersection type system of Barendregt, Coppo and Dezani, thus providing a complete proof of the conjecture, proposed in Leivant (1990), that all functions uniformly definable using intersection types are already definable using Curry types.  
  Address  
  Corporate Author (up) Thesis  
  Publisher Cambridge University Press Place of Publication New York, NY, USA Editor  
  Language Summary Language Original Title  
  Series Editor Series Title Abbreviated Series Title  
  Series Volume Series Issue Edition  
  ISSN 0960-1295 ISBN Medium  
  Area Expedition Conference  
  Notes Approved yes  
  Call Number Sapienza @ mari @ Bucciarelli-Piperno-Salvo:MSCS-03 Serial 69  
Permanent link to this record
Select All    Deselect All
 |   | 
Details
   print

Save Citations:
Export Records: