2026-07-21T18:41:11Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:6567 2024-03-06T10:38:44Z ddc:004 open_access

Polymorphic Game Semantics for Dynamic Binding Laird, James Game semantics denotational models PCF Idealized Algol 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik James Laird 2016 Is Part Of LIPIcs, Volume 62, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2016.27 urn:nbn:de:0030-drops-65671 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.27 eng https://creativecommons.org/licenses/by/3.0/legalcode