A complete realisability semantics for intersection types and infinite expansion variables

Fairouz Dib Kamareddine, Karim Nour, Vincent Rahli, Joseph Brian Wells

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.
Original languageEnglish
Title of host publication 5th International Colloquium on Theoretical Aspects of Computing, ICTAC 2008
PublisherSpringer
VolumeLNCS 5160
Publication statusPublished - 2008

Fingerprint Dive into the research topics of 'A complete realisability semantics for intersection types and infinite expansion variables'. Together they form a unique fingerprint.

Cite this