Semantic Structures for Higher-Order Information Flow

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

The aim of this research is to develop a general theory for describing and reasoning about higher-order programs, which can operate not just on basic data (such as numerical values) but programs themselves (which may also be higher-order programs). These arise in many different settings, but their subtle and complicated nature means that errors and inefficiencies are difficult to identify and rectify or avoid, without a strong theoretical basis for doing so.One way to describe these programs uses mathematical models based on representing programs as strategies in a formal game. This game semantics'' has been used to develop very accurate models and powerful reasoning tools for a wide range of higher-order programming languages - in particular, languages with imperative or mutable variables, which can be used to store data and programs and subsequently updated. However, there is no systematic way of describing these models - proving that they are well-behaved'' must generally be done on a case-by-case basis. This project will investigate a new way of constructing models of such languages, using structures from category theory to capture the dependence of one event'' in a computation on another (for example, reading from a mutable variable returns the last piece of data written to it) in an abstract way. Any instance of these relatively simple structures can be used to construct a model of the associated language, and they can also be used to guarantee that the model captures all observable properties of the language, for example. This will make it easier to find new models and prove their key properties. By developing a calculus for describing the semantic structures which have been identified, the proposed research will yield a novel way to write down higher-order imperative programs themselves, to generate rules for determining when two programs are equivalent (i.e. interchangeable), and to suggest rules for controlling information flow - for example, preventing an update of one variable from changing the value stored in a different one.