Principal Types and Unification for Simple Intersection Type Systems

Mario Coppo, Paola Giannini

Risultato della ricerca: Contributo su rivistaArticolo in rivistapeer review

Abstract

In this paper we introduce a decidable restriction of the intersection type discipline. The restriction is based on a uniform principle rather than on a notion of rank. For this system we give a type checking algorithm that we prove to be sound and complete. An extended language of types with labelled intersections and intersection schemes is needed to describe the principal type of terms which turns out to be unique module a set of equations between labels. The unification algorithm far labelled types, that extends first order unification, could be used as a basis to define inference algorithms for other (more powerful) systems with intersection.

Lingua originaleInglese
pagine (da-a)70-96
Numero di pagine27
RivistaInformation and Computation
Volume122
Numero di pubblicazione1
DOI
Stato di pubblicazionePubblicato - ott 1995
Pubblicato esternamente

Fingerprint

Entra nei temi di ricerca di 'Principal Types and Unification for Simple Intersection Type Systems'. Insieme formano una fingerprint unica.

Cita questo