Game Semantics for a Generic Programming Language

Jim Laird


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.

Thursday 1st July 2010, 14:00
Video Conferencing Room - Far-134
Department of Computer Science