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. © 2010 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
Laird, J. (2010). Game semantics for call-by-value polymorphism. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6199 LNCS, pp. 187–198). https://doi.org/10.1007/978-3-642-14162-1_16
Mendeley helps you to discover research relevant for your work.