Intersection types and λ-definability
Bucciarelli
Antonio
author
Piperno
Adolfo
author
Salvo
Ivano
author
2003
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.
exported from refbase (http://mclab.di.uniroma1.it/publications/show.php?record=69), last updated on Thu, 22 Nov 2012 14:59:18 +0100
text
http://mclab.di.uniroma1.it/publications/papers/papers/Bucciarelli2003.ps
10.1017/S0960129502003833
Bucciarelli_etal2003
Sapienza @ mari @ Bucciarelli-Piperno-Salvo:MSCS-03
Mathematical Structures in Computer Science
2003
Cambridge University Press
New York, NY, USA
continuing
periodical
academic journal
13
1
15
53
0960-1295