Extensional semantics of program behaviour

游戏语义是一种有意对编程语言进行建模的方式：在游戏模型中，程序由它可能与其环境的一系列交互来解释。另一方面，域理论扩展地建模程序，使用某些结构化集合之间的函数。近年来，游戏在建模各种各样的具有一系列复杂功能（如状态和控制操作符）的编程语言方面非常成功。这些模型的显着特点是它们非常精确：模型中的属性与语言中的属性之间存在绝对对应。另一方面，虽然域理论模型很少如此精确，但它们已经被证明是成功的，因为它们易于使用，并且具有丰富的数学理论。域理论（Laird的双稳态概念）的最新发展表明，游戏语义和基于域的语义之间存在密切联系。本项目旨在发现和阐述这些联系：我们将研究如何在域理论环境中进行游戏语义的内涵建模，以及各种不同类型的域如何对应于新类型的游戏。其成果将是一系列新的编程语言模型，以及构建此类模型的技术，以及将游戏与领域联系起来的理论。

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.