In an economy as relentlessly digital as the modern worldwide one, in which everything from toasters to interpersonal communications to global financial services are computerised, the need for formally verified software cannot be overestimated. Formal verification uses mathematical techniques to prove that programs actually perform the computations they are intended to perform (e.g., that text editors really do save files when a SAVE command is issued or that automatic pilots really do correctly execute flight plans) and also avoid performing unintended ones (e.g., leaking credit card details or launching nuclear weapons without authorisation). Since programmers make 15 to 50 errors per 1000 lines of code, and since repairing them accounts for some 80% of project expenses, the ever-increasing size and sophistication of programs makes formal verification increasingly critical to modern software development. Mathematical reasoning lies at the core of all formal verification, and so is crucial for building truly secure and reliable software. One of the key techniques for formally verifying properties of software systems uses logical relations. Logical relations provide a means of deriving properties of a software system directly from the system itself; as a result, they can be used to prove important properties of programs, programming languages, and language implementations. Logical relations have been developed for core fragments of many modern programming languages and verification systems. They are currently extended to richer programming languages and properties by constructing plausible variants of the definitions of logical relations for appropriate core fragments and checking that the mathematical theory goes through. But as languages and properties to be proved have become increasingly sophisticated and expressive, this ad hoc approach has become both difficult and unsustainable. It has also led to an enormous constellation of complicated and non-reusable logical relations that "work" for particular language features, rather than their principled and transferrable development from fundamental principles. In short, logical relations have struggled to keep pace with developments in programming languages, with the obvious consequences for security and reliability of software systems. We aim to revolutionise the landscape of logical relations by providing framework for their development and use that is principled, conceptually simple, reusable, and uniform (rather than ad hoc). Our framework will be capable of both describing the wide array of logical relations already used in existing applications and prescribing new logical relations for future ones. It will be based on the mathematical concept of comprehension for a fibration, which has not previously been identified as a key ingredient in the construction of logical relations. Our use of it thus distinguishes our framework from all other treatments of logical relations in the literature. Comprehension allows explicit representation of logical properties of languages within those languages themselves. This means that our framework will be implementable, so we will produce a logic for deriving consequences of logical relations and a prototype implementation of that logic in a modern interactive theorem prover. This will allow users to experiment with our framework, and allow their experiences with it to feed back into its foundations. We will also apply our new framework for logical relations to cutting-edge problems that are the focus of active research and for which there is presently no consensus on the way forward. Successful application of our framework will show that it can solve problems that are the focus of active research, as well as open up unanticipated new research directions. Conversely, the practical applications we pursue will raise challenges that prompt us to further refine its foundations

This document presents the case for a DTC at Lancaster University, targeting the Digital Economy priority area. Recent government thinking (as witnessed by the Sainsbury, Cox and Denham reviews) highlights the crucial role of innovation and its importance for the future health of the UK economy (including the Digital Economy). We rise to this challenge by proposing a world class, cross-disciplinary and user-centric DTC which places innovation at the heart of its curriculum and ethos. We propose to go beyond traditional multi-disciplinary approaches by seeking a creative fusion between three key disciplines, namely computer science, management and design. The emphasis is on producing a new breed of innovative people who understand and are able to advance the state of the art in technical, design and business innovation (exploring the possible, desirable and feasible). We further propose to align the Centre closely with the needs and goals of industrial producers and consumers of digital innovation (user focus) to ensure the relevance of the PhD programme and to encourage technology transfer/ early adoption of the emerging ideas and knowledge exchange. The DTC will build on the strengths of the InfoLab21 initiative, a recognised leader in technology transfer strategies, in order to seek more valuable and viable technical, social and economic pathways from the laboratory to organisational end-users and producers. The bid also builds on existing support including a Marie Curie Training Network in Creative Design/ Innovation. The long term vision of the centre is to achieve sustainability through partnerships between the university and organisational and customer end users.Key features of the bid include:- A deliberate and distinctive cross-cutting strategy of focusing on innovation as the core of the programme and rooting each PhD within thematic clusters to achieve the desired user focus;- The bringing together of three centres of excellence at Lancaster, namely the Management School, InfoLab21 and ImaginationLancaster with a focus on the resultant creative fusion;- Strong and dedicated leadership offered by 0.5 FTE Director (Prof. Gordon Blair) with significant experience of leadership and postgraduate training;- Location in a new customised space, with value added features such as the Imagination Studio, at a total cost of 10m, building on other investments in the 3 centres of excellence of 38.5m;- Programmes to engage with producers and users of digital innovations, thereby enhancing the student experience through sponsorship, industrial internships and international placements;- Significant focus on SME engagement and their business development, with associated structures and mechanisms becoming a focus for innovation in their own right;- The incorporation of a 12 month Masters of Research (MRes) featuring core modules on innovation, tailorable elements from the three centres, and also a number of ideas factories supporting a refinement from the cross-disciplinary thematic clusters and the definition of MRes and PhD projects; - A requirements-driven transferable skills programme within the 1+3 programme, targeted at industrial needs and capabilities, with the added feature of master classes from inspirational speakers including Sir Chris Bonnington;- Strong programme and quality assurance management, including an emphasis on recruitment.This is a distinctive, bold, imaginative and potentially high impact proposal which can contribute significantly to, and indeed shape, the emerging Digital Economy agenda through its focus on digital innovation. Significant additional contributions are also planned with respect to the Innovation Nation and in particular mechanisms and policies to stimulate innovative thinking in the economy and in society.

The great majority of the CDT's research will fit into the four themes listed below, whether focussed upon application domains or on underpinning research challenges. These represent both notable application areas and emerging cyber security goals, and taken together cover some of the most pressing cyber security challenges our society faces today. 1. Security of 'Big Data' covers the acquisition, management, and exploitation of data in a wide variety of contexts. Security and privacy concerns often arise here - and may conflict with each other - together with issues for public policy and economic concerns. Not only must emerging security challenges be ad-dressed, new potential attack vectors arising from the volume and form of the data, such as enhanced risks of de-anonymisation, must be anticipated - having regard to major technical and design challenges. A major application area for this research is in medical re-search, as the formerly expected boundaries between public data, research, and clinical contexts crumble: in the handling of genomic data, autonomous data collection, and the co-management of personal health data. 2. Cyber-Physical Security considers the integration and interaction of digital and physical environments, and their emergent security properties; particularly relating to sensors, mobile devices, the internet of things, and smart power grids. In this way, we augment conventional security with physical information such as location and time, enabling novel security models. Applications arise in critical infrastructure monitoring, transportation, and assisted living. 3. Effective Systems Verification and Assurance. At its heart, this theme draws on Oxford's longstanding strength in formal methods for modelling and abstraction applied to hardware and software verification, proof of security, and protocol verification. It must al-so address issues in procurement and supply chain management, as well as criminology and malware analysis, high-assurance systems, and systems architectures. 4. Real-Time Security arises in both user-facing and network-facing tools. Continuous authentication, based on user behaviour, can be less intrusive and more effective than commonplace one-time authentication methods. Evolving access control allows decisions to be made based on past behaviour instead of a static policy. Effective use of visual analytics and machine learning can enhance these approaches, and apply to network security management, anomaly detection, and dynamic reconfiguration. These pieces con-tribute in various ways to an integrated goal of situational awareness. These themes link to many existing research strengths of the University, and extend their horizon into areas where technology is rapidly emerging and raising pressing cyber security concerns. The proposal has strong support from a broad sweep of relevant industry sectors, evidenced by letters of support attached from HP Labs, Sophos, Nokia, Barclays, Citrix, Intel, IBM, Microsoft UK, Lockheed Martin, Thales, and the Malvern Cyber Security Cluster of SMEs.