Game semantics for a polymorphic programming language

Research output: Contribution to journalArticlepeer-review

9 Citations (Scopus)
116 Downloads (Pure)

Abstract

This article presents a game semantics for higher-rank polymorphism, leading to a new model of the calculus System F, and a programming language which extends it with mutable variables. In contrast to previous game models of polymorphism, it is quite concrete, extending existing categories of games by a simple development of the notion of question/answer labelling and the associated bracketing condition to represent "copycat links" between positive and negative occurrences of type variables. Some well-known System F encodings of type constructors correspond in our model to simple constructions on games, such as the lifted sum. We characterize the generic types of our model (those for which instantiation reflects denotational equivalence), and show how to construct an interpretation in which all types are generic. We show how mutable variables ( à la Scheme) may be interpreted in our model, allowing the definition of polymorphic objects with local state. By proving definability of finitary elements in this model using a decomposition argument, we establish a full abstraction result.
Original languageEnglish
Article number29
Number of pages27
JournalJournal of the ACM
Volume60
Issue number4
DOIs
Publication statusPublished - Aug 2013

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

Cite this