Game semantics for a polymorphic programming language

Reference:

Laird, J., 2010. Game semantics for a polymorphic programming language. In: 25th Annual IEEE Symposium on Logic in Computer Science, LICS 2010. IEEE, pp. 41-49. (Proceedings - Symposium on Logic in Computer Science)

Related documents:

Official URL:

http://dx.doi.org/10.1109/LICS.2010.32

Abstract

A fully abstract game semantics for an idealized programming language with local state and higher rank polymorphism - System F extended with general references - is described. It quite concrete, and extends existing games models by a simple development of the existing question/answer labelling to represent "copycat links" between positive and negative occurrences of type variables, using a notion of scoping for question moves. 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. 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.

Export

Actions (login required)