Projects per year
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.
|Publication status||Published - 1 Sep 2016|
FingerprintDive into the research topics of 'Polymorphic Game Semantics for Dynamic Binding'. Together they form a unique fingerprint.
- 1 Finished
Semantic Types for Verified Program Behaviour
Engineering and Physical Sciences Research Council
28/02/14 → 31/07/17
Project: Research council