Game semantics for call-by-value polymorphism

Research output: Contribution to journalArticle

4 Citations (SciVal)


A game semantic approach to interpreting call-by-value polymorphism is described, based on extending Hyland-Ong games (which have already proved a rich source of models for higher-order programming languages with computational effects) with explicit "copycat links". This captures universal quantification in a simple and concrete way; it is effectively presentable, and opens the possibility of extending existing model checking techniques to polymorphic types. In particular, we present a fully abstract semantics for a call-by-value language with general references and full higher-rank polymorphism, within which polymorphic objects, for example, may be represented. We prove full abstraction by showing that every universally quantified type is a definable retract of its instantiation with the type of natural numbers.
Original languageEnglish
Pages (from-to)187-198
Number of pages12
JournalLecture Notes in Computer Science
Volume6199 LNCS
Publication statusPublished - Jul 2010
Event37th International Colloquium on Automata, Languages and Programming, ICALP 2010, July 6, 2010 - July 10, 2010 - Bordeaux, France
Duration: 1 Jul 2010 → …

Bibliographical note

AUTOMATA, LANGUAGES AND PROGRAMMING, PT II. 37th International Colloquium on Automata, Languages and Programming, ICALP 2010. 6-10 July 2010. Bordeaux, France.


Dive into the research topics of 'Game semantics for call-by-value polymorphism'. Together they form a unique fingerprint.

Cite this