Abstract
Expansion was introduced at the end of the 1970s for calcu-
lating principal typings for -terms in intersection type systems. Expan-
sion variables (E-variables) were introduced at the end of the 1990s to
simplify and help mechanise expansion. Recently, E-variables have been
further simplified and generalised to also allow calculating other type
operators than just intersection. There has been much work on seman-
tics for intersection type systems, but only one such work on intersection
type systems with E-variables. That work established that building a se-
mantics for E-variables is very challenging. Because it is unclear how to
devise a space of meanings for E-variables, that work developed instead
a space of meanings for types that is hierarchical in the sense of hav-
ing many degrees (denoted by indexes). However, although the indexed
calculus helped identify the serious problems of giving a semantics for
expansion variables, the sound realisability semantics was only complete
when one single E-variable is used and furthermore, the universal type !
was not allowed. In this paper, we are able to overcome these challenges.
We develop a realisability semantics where we allow an arbitrary (possi-
bly infinite) number of expansion variables and where ! is present. We
show the soundness and completeness of our proposed semantics.
lating principal typings for -terms in intersection type systems. Expan-
sion variables (E-variables) were introduced at the end of the 1990s to
simplify and help mechanise expansion. Recently, E-variables have been
further simplified and generalised to also allow calculating other type
operators than just intersection. There has been much work on seman-
tics for intersection type systems, but only one such work on intersection
type systems with E-variables. That work established that building a se-
mantics for E-variables is very challenging. Because it is unclear how to
devise a space of meanings for E-variables, that work developed instead
a space of meanings for types that is hierarchical in the sense of hav-
ing many degrees (denoted by indexes). However, although the indexed
calculus helped identify the serious problems of giving a semantics for
expansion variables, the sound realisability semantics was only complete
when one single E-variable is used and furthermore, the universal type !
was not allowed. In this paper, we are able to overcome these challenges.
We develop a realisability semantics where we allow an arbitrary (possi-
bly infinite) number of expansion variables and where ! is present. We
show the soundness and completeness of our proposed semantics.
| Original language | English |
|---|---|
| Title of host publication | 5th International Colloquium on Theoretical Aspects of Computing, ICTAC 2008 |
| Publisher | Springer |
| Volume | LNCS 5160 |
| Publication status | Published - 2008 |