## 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 |