Skip to Main content Skip to Navigation

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.
Document type :
Complete list of metadata

Cited literature [24 references]  Display  Hide  Download
Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Monday, September 25, 2006 - 3:08:25 PM
Last modification on : Saturday, October 3, 2020 - 3:12:36 AM
Long-term archiving on: : Monday, September 20, 2010 - 4:24:45 PM


  • HAL Id : inria-00096419, version 2


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



Record views


Files downloads