Extensional semantics of program behaviour

点击翻译按钮获取中文摘要

Game semantic is a way of modelling programming languages intentionally: in a games model, a program is interpreted by a sequence of interactions which it may have with its environment. Domain theory, on the other hand, models programs extensionally, using functions between certain structured sets.Games have been very successful in recent years at modelling a wide variety of programming languages with a range of sophisticated features such as state and control operators. The remarkable feature of these models is that they are very precise: there is an absolute correspondence between properties in the model and properties in the language. On the other hand, while domain theoretic models are seldom so precise , they have proved successful in the sense that they are easy to work with and enjoy a rich mathematical theory.Recent developments in domain theory (Laird's notion of bistability) suggest that close connections between game semantics and domain-based semantics are available. This project seeks to discover and elaborate these connections: we will investigate how the intensional modelling of game semantics can be carried out in a domain-theoretic setting, and how the various different kinds of domains correspond to new kinds of games. The outcomes will be a range of new models of programming languages , and techniques for constructing such models, as well as a theory connectinggames to domains.