Game semantics for a polymorphic programming language
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:This repository does not currently have the full-text of this item.
You may be able to access a copy if URLs are provided below.
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.
|Item Type||Book Sections|
|Departments||Faculty of Science > Computer Science|
|Additional Information||25th Annual IEEE Symposium on Logic in Computer Science, LICS 2010. 11-14 July 2010. Edinburgh, UK.|
Actions (login required)