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.