Semantic Types for Verified Program Behaviour

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

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.