Semantic Types for Verified Program Behaviour

类型帮助程序员正确地组合程序组件，避免错误。子类型多态性通过允许不同类型的程序在相同的上下文中安全地使用而增加了灵活性——作为构建程序的一种手段，它已经在面向对象语言中得到了极其广泛和富有成效的应用。二级特性，如有界量化和类型运算符，允许程序员进一步控制在程序之间传递的代码类型，为代码的模块化组合和重用构成了强大的描述性工具。指称语义用于构建编程语言的精确模型，这些模型从实现细节中抽象出来，并允许通过将程序作为数学对象的解释进行推理来证明程序的正确性。该项目旨在使用语义来理解二阶类型系统捕获的高度复杂的结构，同时开发新的能力，使用它们来描述和推理程序的计算行为以及可能对其进行评估的环境：例如，通过限制其对控制或信息流的访问来防止恶意代码危及安全性。它将发展验证这些属性的能力，并在程序的构建中直接或间接地使用证明。它将使用游戏语义研究类型和类型系统，游戏语义根据程序与环境的交互描述程序，作为正式的两玩家游戏。这反映了我们希望推理的行为属性，如控制和信息流，优雅地捕捉了关键的计算副作用，如局部状态，并为其推理提供了强大的算法和操作技术。此外，它还允许对内涵语义子类型的简单概念进行形式化和研究：如果T中的程序行为在S中可用，S中的环境行为在T中可用，则类型S表示T的子类型。通过将其与最近开发的二阶类型作为游戏的内涵表示相结合，该项目将开发新的模型-具有高阶状态，动态绑定，有界量词和类型构造函数的编程语言-使用这些特征来表示程序行为的新类型理论。计算效果和代码可能运行的环境——以及通过模型检查、类型检查和操作方法验证程序属性的新推理技术。

Types help programmers to combine program components correctly, avoiding errors. Subtype polymorphism adds flexibility by allowing programs of different types to be used safely in the same context - as a means of structuring programs it has already found extremely widespread and fruitful application in object-oriented languages. Second-order features such as bounded quantification and type operators allows programmers further control over the type of code which is passed between programs, constituting powerful descriptive tools for the modular combination and reuse of code.Denotational semantics is used to construct precise models of programming languages which abstract away from implementation detail and allows programs to be proved correct by reasoning about their interpretations as mathematical objects. This project aims to use semantics to understand the highly complex structures captured by second-order type systems, while developing the new capacity to use them to describe and reason about computational behaviour of programs and the environments in which they may be evaluated: for example, preventing malicious code from compromising security by constraining its access to control or information flow. It will develop the capacity to verify such properties and to use proofs directly and indirectly in the construction of programs. It will study types and type systems using game semantics, which describes programs in terms of their interaction with the environment, as a formal two player game. This reflects the behavioural properties that we wish to reason about, like control and information flow, elegantly captures key computational side-effects, like local state, and lends itself to powerful algorithmic and operational techniques for reasoning about them. Moreover, it allows a simple notion of intensional semantic subtyping to be formalised and investigated: a type S represents a subtype of T if program behaviour in T is available in S, and environment behaviour in S is available in T. By combining this with recently developed intensional representations of second-order types as games, the project will develop new models - of programming languages with higher-order state, dynamic binding, bounded quantifiers, and type constructors - new type theories using these features to represent program behaviour, computational effects and the environments in which code may be run - and new reasoning techniques for verifying program properties by model checking, type checking, and operational methods.