Software is integral to the fabric of our lives, controlling transport, the economy and infrastructure, and providing the main tools of work and leisure. The cost of software failures is therefore high, to productivity, stability, safety, and privacy. As an indication of the economic impact, it is estimated that software errors cost the US economy tens of billions of dollars last decade. Software errors can also impact human safety as software is used to control transport, infrastructure, and medical equipment. The research agenda of program verification aims to mitigate these risks by putting software engineering on a rigorous foundation through techniques to guarantee program correctness. As software becomes more complex and pervasive, program verification is ever more important. This work aims to advance the state-of-the-art in verification at the point of program development through advancements in programming language theory and practice. Programming languages are the core tool in which software is constructed; they are the means of communicating our intentions to computer hardware. There are various design trade-offs when creating a programming language, which has led to the variety of programming languages in use today. Some languages support verification by including a "type system" which categorises data and operations, ensuring that operations are only applied to data of the correct type. This provides some guarantees about the correctness of the program by ruling out various kinds of error before the program is ever executed. A subfield of programming language research aims to make type systems more expressive so that they can describe and enforce more properties of programs and thus raise the level of verification possible within the language. The current proposal aims to do just this, focussing on the notion of data as a "resource" subject to constraints which should be enforced by a language's type system. This project develops a particular technique for building such type systems in a way that can capture various kinds of property in one system. The manipulation of data is central to the task of programming. Current programming languages essentially view data as an infinitely-replicable resource that can be stored, manipulated, and communicated without restriction. However, this perspective is naive. Some data is private and thus should not be arbitrarily copied, stored, or communicated. Some data is large and thus should not be replicated too frequently. Some data acts as a way of interfacing with other parts of a system, e.g., files or communication channels, which are then subject to restrictions on how they can be used, such as agreed protocols of interaction. Most programming languages are agnostic to these constraints however, treating data as totally unconstrained. This can lead to various software errors, including privacy breaches, performance problems, and crashes due to incorrect interactions between parts of a system. The goal of this research is to embed the constraints associated with data into the type system of a language so that these additional constraints can be automatically enforced. The key technology for doing this is a novel notion of types called "graded modal types" which can capture and track different kinds of information about the structure of programs and the flow of data through them. This work will develop the theory and practice of graded modal types, producing a prototype language that demonstrates their use for verifying program properties. Three case studies will be carried out to demonstrate their power: (1) ensuring privacy and confidentiality, (2) capturing and reasoning about performance e.g., how fast a program will execute relative to the size of its inputs and how much memory it will consume (3) enforcing fine-grained protocols of interaction. This work is a step towards a new generation of trustworthy software.

Passive non-neuronal brain cells called astrocytes have emerged as a critical yet grossly understudied part of brain machinery. Atrocytes take up released neurotransmitters, maintain ionic homeostasis of the extracellular space, and generate a variety of molecular signlas that regulate neural circuit activity. However, the emerging difference between animal and human astroglia in their morphology and physiology threatens the harm-benefit ratio of animal preparations in this important field of neuroscience and neurology. In this respect, realistic computational models of astroglia and astroglia-neuronal networks could provide hypothesis testing, mechanistic physiological insights, and an inter-species knowledge transfer that are unattainable in animal experiments. Exploring such models ought to minimise animal experimentation with no loss of knowledge, yet the methodology to create the corresponding modelling environment is only beginning to emerge. Thus, the present project aims to combine an experimental methodological approach, on the one hand, and open-access computer-simulation platforms, on the other, that would shift the weight of knowledge-based glial research from animals to human tissue preparations and realistic computational models. This will be achieved through the three objectives: (i) to establish working experimental protocols for up-to-date studies of human astroglia in organised brain tissue, making them a commonly accessible, viable alternative to animal brain tissue research strategies, (ii) to create an open-access computational platform that enables exploratory investigation of realistic biophysical models of astroglia, thus reducing similarly aimed experimental trials in animals, and (iii) to generate an experimental data library adaptable for the functional comparison of animal and human astroglia, thus providing a guidance on potentially implausible extrapolation of animal data to human brain astroglia.