(Bath)

I'll describe a new approach to giving games models of programming languages with higher-rank polymorphism. It is based on using question and answer labelling to represent "copycat links" between quantified type variables. The resulting model of System F types is quite concrete --- it is effectively presentable, opening the possibility of extending existing model checking techniques to polymorphic types, for example. It is also a novel example of a model of System F with the genericity property.By adding locally declared general references, we obtain a model of a language in which polymorphic objects may be naturally represented. We prove definability of finite elements, and thus a full abstraction result, using a decomposition argument. This also establishes that terms may be approximated up to observational equivalence when instantiation is restricted to tuples of type variables.

Video Conferencing Room - Far-134

Department of Computer Science