Game semantics and subtyping

While game semantics has been remarkably successful at modelling, often in a fully abstract manner a wide range of features of programming languages, there has to date been no attempt at applying it to subtyping. We show how the simple device of explicitly introducing error values in the syntax of the calculus leads to a notion of subtyping for game semantics. We construct an interpretation of a simple λ-calculus with subtyping and show how the range of the interpretation of types is a complete lattice, thus yielding an interpretation of bounded quantification