System-Level Game Semantics: A unifying framework for composing systems

The recent work on System-Level Games provides a semantic framework for modelling low-level code interactions involving resources shared between a program and its environment.
This project will apply the framework for deriving compositional analysis techniques for software compilation and verification. Semantically, the project will produce a paradigmatic model for programs made of combinations of arbitrary low- and high-level code fragments.
By directly examining the interaction traces of code, as produced by our model, we will extract trace-based analyses based on co-induction, as well as behavioural types governing game plays. By trace analysis we will also produce syntax-independent compilation analyses on tamper-resistance and code linking.
These techniques will be applied on the prototype language Verity and will deliver significant improvements to its existing GOS compiler, which is particularly suitable a test-bench because of its high degree of heterogeneity both in terms of languages (functional vs. hardware) and platforms (CPU-based vs. FPGA).

Cloud computing and heterogeneous computing are widely acknowledged to dominate the software landscape in the foreseeable future.
Our work will contribute directly to making such software sufficiently accessible for non-systems programmers, a line of work acknowledged as a priority direction of development.
Rationalising the burgeoning and chaotic world of APIs has been declared "the future of coding''.
Since computing is becoming the main infrastructure of the economy and of much scientific research, we argue that the impact of this line of work, as generally construed, will be extremely broad.
These considerations apply equally to the international research and economic landscape.