A New Presentation of the Intersection Type Discipline through Principal Typings of Normal Forms

Abstract : We introduce an intersection type system which is a restriction of the intersection type discipline. This restriction leads to a principal type property for normal forms in the classical sense, while retaining the expressivity of the classical discipline. We characterize the structure of principal types of normal forms and give an algorithm that reconstructs normal forms from types. Having shown the equivalence between principal types and normal forms, we define an expansion operation on types which allows us to recover all possible types for any normalizable $\lambda$-term. The contribution of this work is a new and simpler presentation of the intersection type discipline through a purely syntactic and completely characterized notion of principal types.
Type de document :
Rapport
[Research Report] RR-2998, INRIA. 1996
Liste complète des métadonnées

https://hal.inria.fr/inria-00073698
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 13:33:28
Dernière modification le : vendredi 25 mai 2018 - 12:02:03
Document(s) archivé(s) le : dimanche 4 avril 2010 - 21:27:08

Fichiers

Identifiants

  • HAL Id : inria-00073698, version 1

Collections

Citation

Emilie Sayag, Michel Mauny. A New Presentation of the Intersection Type Discipline through Principal Typings of Normal Forms. [Research Report] RR-2998, INRIA. 1996. 〈inria-00073698〉

Partager

Métriques

Consultations de la notice

194

Téléchargements de fichiers

167