The Heart of Intersection Type Assignment

Steffen Van Bakel 1
1 MIMOSA - Migration and mobility : semantics and applications
CRISAM - Inria Sophia Antipolis - Méditerranée , Université de Provence - Aix-Marseille 1, MINES ParisTech - École nationale supérieure des mines de Paris
Abstract : This paper gives a new proof for the approximation theorem and the characterisation of normalisability using intersection types. The technique applied is to define reduction on derivations and to show a strong normalisation result for this reduction. From this result, the characterisation of strong normalisation and the approximation result will follow easily; the latter, in its turn, will lead to the characterisation of (head-)normalisability.
Type de document :
Rapport
[Research Report] RR-5984, INRIA. 2006, pp.34
Liste complète des métadonnées

Littérature citée [24 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00096419
Contributeur : Rapport de Recherche Inria <>
Soumis le : lundi 25 septembre 2006 - 15:08:25
Dernière modification le : samedi 27 janvier 2018 - 01:31:25
Document(s) archivé(s) le : lundi 20 septembre 2010 - 16:24:45

Fichier

Identifiants

  • HAL Id : inria-00096419, version 2

Citation

Steffen Van Bakel. The Heart of Intersection Type Assignment. [Research Report] RR-5984, INRIA. 2006, pp.34. 〈inria-00096419v2〉

Partager

Métriques

Consultations de la notice

183

Téléchargements de fichiers

101