Game semantics for bounded polymorphism

Research output: Chapter in Book/Report/Conference proceedingConference contribution

104 Downloads (Pure)

Abstract

We describe a denotational, intensional semantics for programs with polymorphic types with bounded quantification, in which phenomena such as inheritance between stateful objects may be represented and studied. Our model is developed from a game semantics for unbounded polymorphism, by establishing dinaturality properties of generic strategies, and using them to give a new construction for interpreting subtyping constraints and bounded quantification. We use this construction to give a denotational semantics for a programming language with general references and an expressive polymorphic typing system. We show that full abstraction fails in general in this model, but that it holds for all terms at a rich collection of bounded types.

Original languageEnglish
Title of host publicationFoundations of Software Science and Computation Structures. FOSSACS 2016.
Subtitle of host publicationProceedings of 19th International Conference, FOSSACS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, Etaps 2016, Eindhoven, the Netherlands, April 2-8, 2016.
EditorsB. Jacobs, C. Loding
Place of PublicationThe Netherlands
PublisherSpringer Verlag
Pages55-70
Number of pages16
ISBN (Print)9783662496299
DOIs
Publication statusPublished - 22 Mar 2016
Event19th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2016 and Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016 - Eindhoven, Netherlands
Duration: 2 Apr 20168 Apr 2016

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume9634

Conference

Conference19th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2016 and Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016
CountryNetherlands
CityEindhoven
Period2/04/168/04/16

Fingerprint Dive into the research topics of 'Game semantics for bounded polymorphism'. Together they form a unique fingerprint.

  • Projects

  • Profiles

    Cite this

    Laird, J. (2016). Game semantics for bounded polymorphism. In B. Jacobs, & C. Loding (Eds.), Foundations of Software Science and Computation Structures. FOSSACS 2016.: Proceedings of 19th International Conference, FOSSACS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, Etaps 2016, Eindhoven, the Netherlands, April 2-8, 2016. (pp. 55-70). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9634). Springer Verlag. https://doi.org/10.1007/978-3-662-49630-5_4