License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2016.27
URN: urn:nbn:de:0030-drops-65671
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2016/6567/
Go to the corresponding LIPIcs Volume Portal

Laird, James

Polymorphic Game Semantics for Dynamic Binding

pdf-format:
LIPIcs-CSL-2016-27.pdf (0.6 MB)

Abstract

We present a game semantics for an expressive typing system for block-structured programs with late binding of variables and System F style polymorphism. As well as generic programs and abstract datatypes, this combination may be used to represent behaviour such as dynamic dispatch and method overriding.

We give a denotational models for a hierarchy of programming languages based on our typing system, including variants of PCF and Idealized Algol. These are obtained by extending polymorphic game semantics to block-structured programs. We show that the categorical structure of our models can be used to give a new interpretation of dynamic binding, and establish definability properties by imposing constraints which are identical or similar to those used to characterize definability in PCF (innocence, well-bracketing, determinacy). Moreover, relaxing these can similarly allow the interpretation of side-effects (state, control, non-determinism) - we show that in particular we may obtain a fully abstract semantics of polymorphic Idealized Algol with dynamic binding by following exactly the methodology employed in the simply-typed case.

BibTeX - Entry

@InProceedings{laird:LIPIcs:2016:6567,
  author =	{James Laird},
  title =	{{Polymorphic Game Semantics for Dynamic Binding}},
  booktitle =	{25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
  pages =	{27:1--27:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-022-4},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{62},
  editor =	{Jean-Marc Talbot and Laurent Regnier},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2016/6567},
  URN =		{urn:nbn:de:0030-drops-65671},
  doi =		{10.4230/LIPIcs.CSL.2016.27},
  annote =	{Keywords: Game semantics, denotational models, PCF, Idealized Algol}
}

Keywords: Game semantics, denotational models, PCF, Idealized Algol
Collection: 25th EACSL Annual Conference on Computer Science Logic (CSL 2016)
Issue Date: 2016
Date of publication: 29.08.2016

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI