Program Reasoning with Nominal Game Semantics

While in recent years great strides have been made in software verification, most of these successes have targeted programming languages of a strong imperative flavour. However, there is an emerging class of languages using higher-order features to cater for well-structured and disciplined programming outputs, for which verification methods are very scarce. In such higher-order languages, capturing formally the behaviour of programs is highly non-trivial and, therefore, even simple program analysis tasks prove to be surprisingly daunting.

This project will combine the latest techniques from game semantics with successful verification approaches from the imperative setting in order to achieve a novel reasoning methodology for higher-order languages. Game semantics is a theory of computation that has emerged as a robust paradigm for assigning formal mathematical semantics to higher-order programs. Game models offer a particularly suitable foundation for program analysis as they combine two features of focal importance: abstraction and compositionality. The former is achieved by focussing only on observable program behaviours, which significantly reduces the examined state-space of programs. The latter amounts to modelling compound program phrases by canonically combining the models of their respective sub-phrases, which in turn allows for the independent analysis of program components and enables local reasoning techniques.

The major obstacle in applying game semantics to real program analysis has been the modelling of dynamic generative effects, involving the generation of fresh references, objects, channels, etc. This issue has been addressed by a recent breakthrough that introduced atomic objects, called "names", in games for representing datatypes of dynamically generated resources. Names led to the introduction of a new strand of the theory called Nominal Game Semantics. Nominal games have extended the reach of game models to realistic higher-order languages and have brought the field to the point where one can start developing formal reasoning methods for such languages.

Our research will take the theory of game semantics to the next level and apply it to program reasoning. Our aim is to derive practical program logics for higher-order programs, equipped with high-level rules enabling abstraction and local reasoning, and complement them with a prototype implementation. The overall vision behind this proposal is to exploit the strong handle on higher-order computation provided by the nominal approach to game semantics in order to significantly extend the reach of modern approaches to verification and aid the production of better software.

Software systems have become an integral part of the infrastructure of our society and control almost every aspect of our lives. Hence, verification and correctness are nowadays far from marginal software requirements concerning solely safety-critical systems. Rather, they are desiderata of software development in general: they concern widespread applications written in a variety of programming languages. The verification problem for such languages poses new challenges as high-level programming features (references, higher-order functions, etc) require accurate handling. Moreover, realistic applications can expand to millions of lines of code, thus demanding decidedly scalable methods.

Our project will achieve the introduction and prototype implementation of a new methodology for reasoning about higher-order programs. Because of its novel ingredients, namely the combination of precise abstractions, compositionality and focus on local reasoning, we hope to contribute techniques that will influence verification standards. By adopting more refined semantic models, we give space to methods which start from a higher level of accuracy and abstraction. By founding our approach on compositional models and reasoning in local environments, we anticipate substantial gains in scalability.

Higher-order programming languages have seen a surge of interest in recent years, with specific applications coming from security-sensitive domains like the finance sector. Hence, the development of verification methods and tools for such languages is of major interest to the industry. Until now, such methods and tools have been very scarce, as the analysis of higher-order programs is a daunting task. Our proposal aims at addressing this shortcoming using the unique advantages of program models obtained from game semantics, and nominal game semantics in particular.

In order to inform all interested parties about our approach, we have planned regular attendance of relevant conferences and workshops, research visits to groups pursuing related state-of-the-art research, and the organisation of a workshop devoted to program logics for higher-order program verification. The latter has been scheduled for the end of the first year of the project. It will coincide with the expected completion of the main tasks from the program logic work packages, when it will be possible to convey the core of our approach. Further connections will be made through visits to academic and industrial labs to give presentations. To that end we are going to exploit existing academic (e.g. Wessex Theory, Joint Theory Seminar) and industrial (e.g. Facebook, Microsoft) links at Queen Mary, as well as personal contacts made at conferences and the workshop.

As our project is of a foundational nature, the main short-term beneficiaries will be other researchers in academia and industry. In the longer term, we would like to see our approach incorporated into mainstream verification tools. Ultimately, we expect the work to impact actual system developers and, consequently, users at large.