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, July 11, 2010 - July 14, 2010, 2010-07-01, Edinburgh. 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. (Contact Author)
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||Conference or Workshop Items (UNSPECIFIED)|
|Departments||Faculty of Science > Computer Science|
Actions (login required)