Research

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:

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.

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.

Details

Item Type Book Sections
CreatorsLaird, J.
DOI10.1109/LICS.2010.32
DepartmentsFaculty of Science > Computer Science
StatusPublished
ID Code22047
Additional Information25th Annual IEEE Symposium on Logic in Computer Science, LICS 2010. 11-14 July 2010. Edinburgh, UK.

Export

Actions (login required)

View Item