Projects per year
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.
|Title of host publication||25th Annual IEEE Symposium on Logic in Computer Science, LICS 2010|
|Number of pages||9|
|Publication status||Published - 2010|
|Event||25th Annual IEEE Symposium on Logic in Computer Science, LICS 2010, July 11, 2010 - July 14, 2010 - Edinburgh, UK United Kingdom|
Duration: 1 Jul 2010 → …
|Name||Proceedings - Symposium on Logic in Computer Science|
|Conference||25th Annual IEEE Symposium on Logic in Computer Science, LICS 2010, July 11, 2010 - July 14, 2010|
|Country/Territory||UK United Kingdom|
|Period||1/07/10 → …|
FingerprintDive into the research topics of 'Game semantics for a polymorphic programming language'. Together they form a unique fingerprint.
- 1 Finished
20/06/10 → 19/06/12
Project: Research council