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 :
Reports
Complete list of metadatas

Cited literature [24 references]  Display  Hide  Download

https://hal.inria.fr/inria-00096419
Contributor : Rapport de Recherche Inria <>
Submitted on : Monday, September 25, 2006 - 3:08:25 PM
Last modification on : Monday, November 12, 2018 - 11:02:13 AM
Long-term archiving on: Monday, September 20, 2010 - 4:24:45 PM

Identifiers

  • 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⟩

Share

Metrics

Record views

219

Files downloads

117