Hostname: page-component-7c8c6479df-995ml Total loading time: 0 Render date: 2024-03-19T10:49:43.149Z Has data issue: false hasContentIssue false

Intersection types and λ-definability

Published online by Cambridge University Press:  06 March 2003

ANTONIO BUCCIARELLI
Affiliation:
PPS, Université Paris 7, 2 Place Jussieu, 75251 Paris Cedex 05, France Email: buccia@pps.jussieu.fr
ADOLFO PIPERNO
Affiliation:
Dipartimento di Scienze dell'Informazione, Università di Roma ‘La Sapienza’, Via Salaria 113, 00198 Roma, Italy Email: piperno@dsi.uniroma1.it
IVANO SALVO
Affiliation:
Dipartimento di Informatica, Università di Torino, C.so Svizzera 185, 10149 Torino, Italy Email: salvo@di.unito.it

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.

Type
Research Article
Copyright
© 2003 Cambridge University Press

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)