Edinburgh Research Archive >
Informatics, School of >
Informatics thesis and dissertation collection >
Please use this identifier to cite or link to this item:
|Title: ||Game Semantics and Subtyping|
|Authors: ||Chroboczek, Juliusz|
|Supervisor(s): ||Abramsky, Samson|
|Issue Date: ||Jul-2003|
|Publisher: ||University of Edinburgh. College of Science and Engineering. School of Informatics.|
|Abstract: ||Game Semantics is a relatively new framework for the description of the semantics of programming languages. By combining the mathematical elegance of Denotational Semantics with explicitly operational concepts, Game Semantics has made possible the direct and intuitive modelling of a large range of programming constructs.
In this thesis, we show how Game Semantics is able to model subtyping. We start by designing an untyped λ-calculus with ground values that explicitly internalises the notion of typing error. We then equip this calculus with a rich typing system that includes quantification (both universal and existential) as well as recursive types.
In a second part, we show how to interpret the untyped calculus; after equipping the domain of the interpretation with an ordering --- the liveness ordering --- loosely inspired from implication on process specifications, we show how our interpretation is both sound and computationally adequate.
In a third part, we introduce a notion of game which we use for interpreting types, and show how the liveness ordering on games is suitable for interpreting subtyping. Finally, we prove that under the (unproved) assumption that recursive types are compatible with quantification, our interpretation is sound with respect to both subtyping and typing.|
|Appears in Collections:||Informatics thesis and dissertation collection|
Items in ERA are protected by copyright, with all rights reserved, unless otherwise indicated.