Dinaturality Meets Genericity: A Game Semantics of Bounded Polymorphism

Research output: Chapter or section in a book/report/conference proceedingChapter in a published conference proceeding

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.

Original languageEnglish
Title of host publication8th International Conference on Formal Structures for Computation and Deduction, FSCD 2023
EditorsMarco Gaboardi, Femke van Raamsdonk
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
ISBN (Electronic)9783959772778
DOIs
Publication statusPublished - 28 Jun 2023
Event8th International Conference on Formal Structures for Computation and Deduction, FSCD 2023 - Rome, Italy
Duration: 3 Jul 20236 Jul 2023

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
Volume260
ISSN (Print)1868-8969

Conference

Conference8th International Conference on Formal Structures for Computation and Deduction, FSCD 2023
Country/TerritoryItaly
CityRome
Period3/07/236/07/23

Keywords

  • Bounded Polymorphism
  • Dinaturality
  • Game Semantics
  • Subtyping

ASJC Scopus subject areas

  • Software

Fingerprint

Dive into the research topics of 'Dinaturality Meets Genericity: A Game Semantics of Bounded Polymorphism'. Together they form a unique fingerprint.

Cite this