License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2023.33
URN: urn:nbn:de:0030-drops-180171
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/18017/
Go to the corresponding LIPIcs Volume Portal

Laird, James

Dinaturality Meets Genericity: A Game Semantics of Bounded Polymorphism

pdf-format:
LIPIcs-FSCD-2023-33.pdf (0.8 MB)

Abstract

We study subtyping and parametric polymorphism, with the aim of providing direct and tractable semantic representations of type systems with these expressive features. The liveness order uses the Player-Opponent duality of game semantics to give a simple representation of subtyping: we generalize it to include graphs extracted directly from second-order intuitionistic types, and use the resulting complete lattice to interpret bounded polymorphic types in the style of System F_<:, but with a more tractable subtyping relation.
To extend this to a semantics of terms, we use the type-derived graphs as arenas, on which strategies correspond to dinatural transformations with respect to the canonical coercions ("on the nose" copycats) induced by the liveness ordering. This relationship between the interpretation of generic and subtype polymorphism thus provides the basis of the semantics of our type system.

BibTeX - Entry

@InProceedings{laird:LIPIcs.FSCD.2023.33,
  author =	{Laird, James},
  title =	{{Dinaturality Meets Genericity: A Game Semantics of Bounded Polymorphism}},
  booktitle =	{8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
  pages =	{33:1--33:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-277-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{260},
  editor =	{Gaboardi, Marco and van Raamsdonk, Femke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2023/18017},
  URN =		{urn:nbn:de:0030-drops-180171},
  doi =		{10.4230/LIPIcs.FSCD.2023.33},
  annote =	{Keywords: Subtyping, Bounded Polymorphism, Game Semantics, Dinaturality}
}

Keywords: Subtyping, Bounded Polymorphism, Game Semantics, Dinaturality
Collection: 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)
Issue Date: 2023
Date of publication: 28.06.2023

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