Game semantics for a polymorphic programming language

Research output: Chapter in Book/Report/Conference proceedingConference contribution

6 Citations (Scopus)

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.
Original languageEnglish
Title of host publication25th Annual IEEE Symposium on Logic in Computer Science, LICS 2010
PublisherIEEE
Pages41-49
Number of pages9
ISBN (Electronic)9781424475896
ISBN (Print)9781424475889
DOIs
Publication statusPublished - 2010
Event25th Annual IEEE Symposium on Logic in Computer Science, LICS 2010, July 11, 2010 - July 14, 2010 - Edinburgh, UK United Kingdom
Duration: 1 Jul 2010 → …

Publication series

NameProceedings - Symposium on Logic in Computer Science

Conference

Conference25th Annual IEEE Symposium on Logic in Computer Science, LICS 2010, July 11, 2010 - July 14, 2010
CountryUK United Kingdom
CityEdinburgh
Period1/07/10 → …

Fingerprint Dive into the research topics of 'Game semantics for a polymorphic programming language'. Together they form a unique fingerprint.

Cite this