PhD opportunities in Computer Science

Stipend: £21,400 per year tax free for 3.5 years

Start date: September 2025 (but preferably sooner)

Supervisors: Mike Chantler, HWU Computer Science; Richard Carter, HWU/EPS; Jonathon Corney, Edinburgh University

Eligibility: Must be UK citizen or have UK settled status, and have equivalent of First class or 2:1 BSc degree in Computer Science.

Project Description: Laser alignment is a highly specialised complex task performed by skilled technicians involving 100s of steps over several days.

Machine learning (ML), when combined with mechatronic controls, offers rapid solution of one- or two-dimensional alignment steps, but also offers the potential to combine steps by optimising over multiple dimensions simultaneously, significantly reducing assembly time.

In order to provide confidence in the algorithms and fully understand how they will be incorporated into alignment procedures it is critical that ML behaviours are both transparent and understandable. Unfortunately, the multidimensional solutions typically provided by ML algorithms are often confusing and opaque.

The project would therefore involve:

Investigate the trade-offs between reducing the complexity and dimensionality of different ML algorithms versus their interpretability and performance.

Develop intuitive visualisation and configuration interfaces, that allow non-ML experts, to investigate and trade off the complexity of solutions, such that they are understandable and can be easily and reliably incorporated into their procedures.

The ML methods that we would target in the first instance would be reinforcement learning and convolutional neural networks. For the former we would investigate ways of biasing the policies in order to produce simpler behaviours (e.g. by favouring exploitation over exploration, or by favouring low-dimensional exploration over high-dimensional search). For the latter we would investigate reducing their structural complexity (e.g. number of FIR filters, number of levels, complexity of the fully connected layers, and employing explicit feature engineering). In addition, we would seek to use visualisation techniques that simplify the visual task for the viewer (e.g.by employing dimensionality reduction techniques, time curves, and matrix scatter displays).

For More Information: Email Mike Chantler, m.j.chantler@hw.ac.uk with CV.

Knowledge Graphs for Biomedical Image Data Management, Integration and Analysis

Supervisor: Albert Burger

Description: Biomedical images play a key role in research as well as clinical practice. A variety of imaging techniques are now available to study healthy as well as diseased tissue in human and model organisms, ranging from cell level to entire organs and organisms. In the clinical context, imaging diagnostics, such as MRI and CT scans, are now routinely used to better understand a patient's medical condition. To be able to take full advantage of the large image respositories that result from this, the information embedded in such images must be computationally represented. This is relevant for image retrieval, data integration and machine learning applications. Knowledge Graphs, a combination of graph-based data management and artificial intelligence, have emerged as a primary technique to model and capture such information, but many questions remain in terms of how to model the information in biomedical images and how to integrate and prepare them for machine learning based studies.  A variety of PhD topics are available in this area, including using knowledge graphs to model anatomical knowledge, integrating cinical image data sets across multiple patients, graph-based machine learning for biomedical images, and using Natural Language Processing techinques to integrate images with medical reports and publications.  If you are interested in discussing any of the above or other related topics for PhD study, please contact Prof Albert Burger.

Equally Safe Online – Multimodal Harmful Content Detection

Supervisors: Verena Rieser, Alessandro Suglia

Description: This project will develop novel multimodal algorithms to detect hateful and toxic content online automatically.  While current approaches solely focus on written text, this project will account for the fact that a large amount of social media posts involve several modalities (such as memes, videos) that carry information – which in their composition can result in harmful meaning. The objective of this project is to design and implement Deep Learning models for Multimodal Harmful Content detection that can be useful to moderate online content and make online spaces safer for Internet users.

Fair Graph Neural Architecture Search

Supervisor: Wei Pang

Description: This project will develop robust graph neural networks which can make fair and effective decisions. To achieve this, we will use multi-objective optimization techniques to make trade-off design solutions for graph neural networks. We will also explore the use of bio-inspired algorithms, such as evolutionary computing and immune-inspired computing algorithms to facilitate the search for suitable graph neural architectures. 

Vision-based surgical robot for interventional vascular surgery

Supervisor: Chengjia Wang

Description: Introduction of robotic procedures has brought significant benefits to intervention vascular surgery with remotely conducted precise procedures and reduced exposure to radiation for clinicians. In the meantime, renaissance of AI in the past decade has fundamentally reshaped many fields with escalated performance in computer vision, natural language processing and other tasks. However, many challenges exists in robot aided vascular surgery, for example, lack of annotated data, reduced sensor feedback, requirement of real-time intra-operation prediction etc.. In this project, you will explore the development of autonomous surgical robot which combining multi-modal sensor data to assist interventional vascular surgery. This involves investigation of frontier designs of surgical robotics tool, development and exploration of advanced deep learning models, fast fusion and visualisation of multi-modality sensory data (e.g., haptics, digital subtraction angiography, and other vascular imaging data), and a full understand of operational procedures in the treatment of vascular disease. 

Robot aid autonomous retrosynthesis for advanced drug discovery

Supervisor: Chengjia Wang

Description: As a fundamental problem in chemistry, Retrosynthesis is the process of decomposing a target molecule into readily available starting materials. It aims at designing reaction pathways and intermediates for a target compound. The goal of artificial intelligence (AI)-aided retrosynthesis is to automate this process by learning from the previous chemical reactions to make new predictions. Although several models have demonstrated their potentials for automated retrosynthesis, there is still a significant need to further enhance the prediction accuracy to a more practical level. This project aims to review, implement and review existing retrosynthesis methods and exploring the development of an autonomous verification robot for retrosynthecial process.

Decentralised, privacy-preserving and explainable federated learning for annotation effective medical image analysis

Supervisors: Chengjia Wang and Wei Pang

Description: Several infectious diseases have attacked human society since the beginning of Since the beginning of this millennium, in the meantime advanced AI models have been widely deployed to assist a variety of tasks for the fight against these global pandemics. Modern clinical studies, especially for popular disease that affect a large cohort of patients, are often requires a collaboration among multiple research centres with large-scale machine learning models applied to analyse distributedly stored clinical data acquired at different sites. Protection of privacy, effective model supervision and interpretability of prediction results are critical in clinical practices while a trade-off exists between any two of them. Furthermore, the required computing power for training the machine learning models can easily exceed the capacity of modern computing devices in clinical centres. This project aims to investigate training and deployment of decentralised federated learning scheme for large scale deep learning models with good adhoc or posthoc interpretability and minimal data exchange between sites. Specifically, the student will explore and development frontier research of image understanding, federated learning, decentralised semi- or weakly- supervise, model compression, heterogeneous data/model distillation, domain adaptation, XAI and possibly advanced blockchain technology.

Swarm bots and swarm intelligence in healthcare internet of things

Supervisors: Chengjia Wang and Wei Pang

Description: Internet of things offer a number of new opportunities to improve patient outcomes through real-time patient monitoring, advanced diagnostics, robotic surgery, and much more. However, the computing power of the associated IoT devices can limit the performance and scale and inference speed of adoptable machine learning models in practice. This is common in complicated robotic surgery and monitoring of high-risk patients, e.g., in ICU. In this project, we aim at development of swarm intelligence methods, empowered by modern deep learning models, that can coordinate a group of intelligent devices for event recognition and decision making. This involves deliberate management of computing capacity, communication, collaborated training and abnormality detection among a heterogeneous group of devices, and further developing the theoretical model into a group of well coordinated swarm bots.

Reference: C.Wang et al., Industrial Cyber-Physical Systems-based Cloud IoT Edge for Knowledge Distillation, IEEE-TII 2021

Enhancing Confidence in Topic Models using Ensembles 

Supervisor: Pierre Le Bras

Description: Topic modelling techniques typically rely on stochastic methods to explore large corpora and solve the multi-dimensional problem of identifying the themes discussed in documents in an unsupervised fashion. These approaches then propose one sample solution, out of many equally likely other solutions. While this is acceptable in most scenarios, confirmed users can still challenge the solution presented to them. 

This project aims to address such limitation by investigating the use of ensemble methods in topic modelling. While some techniques have been described, such as term co-association and topic alignment, ensemble modelling offers other methods that could be applied or adapted to topic modelling. The initial stages of this project will mostly involve the development of data mining algorithms; however, the final goal should be to also investigate means of intuitive visualisations of ensemble topic models and evaluate their impact on user acceptance and confidence. 

Machine/Deep Learning Applied to Neurodegenerative Diseases 

Supervisor: Marta Vallejo

Description: Are you interested in the intersection between neurodegenerative diseases and machine/deep learning?  At the ML-Health group, we are offering PhD projects that contribute to understanding and combating neurodegenerative diseases. 

Project 1: Advancing Diagnosis, Prognosis and Disease Progression in Parkinson’s and Huntington’s Disease. Join us in exploring the potential of wearable data for improving the diagnosis, prognosis, and disease progression of Parkinson's and Huntington's diseases. Collaborative opportunities exist with the University of York and partners in the Netherlands, Germany, and Australia. 

Project 2: Unravelling ALS/Motor Neuron Disease and Protein Aggregation. Work closely with experts from the University of Edinburgh and Aberdeen University to investigate protein aggregation using brain imaging techniques in ALS/Motor Neuron Disease. 

Relevant Techniques: 

• Classification (including CNNs, LSTM..) 
• Segmentation (such as U-Net, Yolo style networks) 
• Data augmentation (utilising GANs) 
• Disease representation (Graph neural networks) 
• Network optimisation (Neuroevolution) 
• Interpretability 

We also encourage exploration of other deep learning-related areas. 

Fair and Ethical Human-Centred NLP

Supervisor: Gavin Abercrombie

Description: From supervised classification and reinforcement-learning with human feedback (RLHF) to the data used to train large language models (LLMs), natural language processing (NLP) relies on data created by humans, but often produces inequitable results for different people. This project will combine computer science, linguistics, cognitive science, and human-centred design practices to investigate annotation and data practices and language modelling algorithms in order to create fair and ethical NLP systems.

Safer Conversational AI

Supervisor: Verena Rieser

Description: Neural models for Conversational AI (ConvAI) and Natural Language Generation (NLG) are known to produce natural and fluent output, however the content is often bland, factually inconsistent, or inappropriate. This research will investigate how to create safer ConvAI models -- e.g. by developing advances in statistical modelling, data curation, evaluation metrics as well as wider design decisions, such as AI persona design.

This project is highly interdisciplinary and reaches from pushing the boundaries of state-of-the-art Machine Learning and statistical modelling to AI Ethics and anticipating the social impacts of AI. Applicants with an interest in either or both of these fields are encouraged to apply.

Generating counterspeech against online hate

Supervisors: Verena Rieser (1st), Ioannis Konstas (2nd)

Description: This project will develop countermeasures to effectively fight the ever-increasing online hate speech without blocking freedom of speech. In particular, it will develop Natural Language Generation algorithms to automatically generate counterspeech -- a response that provides non-negative feedback through fact-bound arguments and broader perspectives to mitigate hate speech and fostering a more harmonious conversation on social platforms. The project requires skills and expertise in deep learning frameworks, as well as knowledge of experimental design and data collection. The PhD project will be embedded in a large, multi-site and multi-disciplinary research project funded by the EPSRC.

Human-Robot Collaboration in Outdoor Environments

Supervisor: Phil Bartie

Description: Autonomous robots will offer the ability to support humans in outdoor environments via a wide variety of roles from rapid delivery of medical equipment via drones, to autonomous cars, to disaster emergency response. All of these need an interface to enable the user to set the robot’s goal, which often includes a destination location. This could be done via a mobile app (eg map interface) or web page, but a more natural way would be to use speech to converse with the device in setting a goal.  Human-robot interaction via voice enhances a robot’s ability to collaborate naturally and seamlessly with humans on joint tasks, e.g. by joint goal setting, communicating progress or clarifying the user’s intention. This research will focus on delivering the ability to generate and parse descriptions of 3D real world objects found in outdoor environments such as buildings, paths, parks, fields and other geographic features for the purpose of human-robot collaboration.

Grounded, Faithful and Transparent Natural Language Generation

Supervisor: Ioannis Konstas, Verena Rieser, Arash Eshghi

Description: This project will focus on the factual correctness of automatically generated text using Deep Learning. In particular, it will build Neural Natural Language Generation models with an emphasis on groundedness and faithfulness to the input source (e.g., news article, a question from a user, knowledge-base), as well as the ability to offer transparency and explainability in the form of attributions and reasoning rationales. The application domains we will explore can range from text summarisation to (conversational) question answering and will require skills and expertise in Natural Language Processing and deep learning frameworks such as PyTorch. 

Modelling Meaning Coordination in Situated Conversational AI

Supervisor: Alessandro Suglia, Arash Eshghi

Description: Human dialogue is rife with miscommunication because people often understand different things from words, have different perspectives, different cultural backgrounds, different skills, etc. The reason they manage to communicate successfully at all is that they put extra interactional effort to coordinate and make sure they understand each other sufficiently for current purposes; and that languages are universally equipped with highly systematised, meta-communicative procedures (known collectively as ‘repair’) such as clarificational exchanges, corrections and demonstrations. While the crucial role of these repair phenomena in sustaining a successful dialogue is widely recognised in Conversation Analysis and Cognitive Science, researchers in Natural Language Processing (NLP) and Human Robot Interaction (HRI) have paid relatively little attention to it so far. State of the art neural architectures that underly conversational AI systems today remain static at run time, don’t learn from the outcome of their actions, and are unable to handle miscommunication. From a Deep Learning perspective, it remains unclear how neural representations or word/sentence embeddings should be updated on the fly as a result of repairs and as part of a live interaction. Grounded in theories of miscommunication and repair in Cognitive Science, this project will investigate the suitability of existing neural architectures, objectives functions, and tasks for modelling meaning coordination in situated dialogue. If successful, the project will be an important stepping stone in the creation of Conversational AI systems that can successfully collaborate with humans in complex situated tasks. 

The Application of Cyber Security Countermeasures to Secure Healthcare Robots

Supervisors: Prof Lynne Baillie and Dr Manuel Maarek

Robotics technology is nowadays becoming widely used in different sectors: healthcare, military, household, construction, and many more. From a security point of view, the threat of unauthorized disclosure to the robot system violates the confidentiality of a patient. The threat by unauthorized parties to patient data and the robot itself violates the integrity of the system. For that reason, investigating what security a robot system to be used in healthcare will need is a top priority to ensure that the sensors, physical robot, the robot system, users, and connected third-party systems are all secured and that all the sources of threats are addressed with corresponding defence mechanisms through the appropriate security and risk models. Any security mechanisims must work well for and be understood by the end user who will interact with the system. The user involvement in the design and development of any solutions is paramount as it has been found that if security solutions do not work well for the end user then they are simply not adopted. This project will work in collaboration with a healthcare EPSRC funded project which is investigating how we can use robots and sensors to diagnose a specific health condition.

Developing Socially Assistive Robots that can Deliver Cognitive Assessments in Care Settings 

Supervisor: Lynne Baillie 

Description: Current assessment methods have subjective measures to assess cognition. For example, the CAM-ICU uses the Richmond Agitation Sedation Scale (RASS) which is a subjective measure of the patient's agitation level. The assessment is subjective and the outcomes different based on who administers the test. The aim of this PhD is to develop and evaluate a novel system for early assessment of the CAM-ICU or similar cognition tests (e.g. 4AT) in vulnerable populations, such as those receiving care in the ICU or assistive living care homes, facilitated by socially assistive robots and Machine Learning. 

Social and Rehabilitation Robots to Assist Sports Rehabilitation 

Supervisor: Lynne Baillie 

Description: There are five phases of rehabilitation, and the aim of this PhD will be to work with a Human Robot Interaction expert and a sports physiotherapist to improve the adherence of sports professionals during 2 key phases of their rehabilitation. The two phases are: improving the range of motion and/or flexibility and improving strength and balance.  

The main aim of this PhD is to explore the potential of using an adaptive robotic coaching system to increase adherence in individual sports rehabilitation in two key phases. The PhD student will have the choice on which areas too focus on. For example: what strategies can be used by an adaptive robotic coaching system to effectively motivate people to adhere to their rehabilitation? Or does adapting the interaction feedback to the sports player increase adherence to exercise? Finally does high-level personalisation, based on user information and training context, improve adherence through adaption to individuals using reinforcement learning? 

Using rhythm for physical rehabilitation

Supervisor: Dr Theodoros Georgiou 

Description: It is a known fact that rhythm can be used help during rehabilitation of many neurological conditions such as hemiparesis, Huntington’s disease, and Parkinson’s disease. Due to the ease of application, rhythm is most commonly applied to patients during sessions with their physiotherapist through auditory means. However, there are situations where this may not be desirable where social and environmental awareness is important.

Aim will be to explore other methods and modalities of introducing rhythm for rehabilitation purposes, such as through the haptic and the visual channel. The successful PhD candidate will have access to rehabilitation equipment located at the National Robotarium as well as facilities to explore prototype solutions for their studies.

This PhD project is highly interdisciplinary, and the successful PhD candidate will need to have a strong background in HCI methods and the ability to learn how to implement prototype software solutions on commercially available rehabilitation hardware.

Please don't hesitate to contact me at T.Georgiou@hw.ac.uk for an informal discussion about this project and how our interests fit together.

Technology assisted rehabilitation with wearables

Supervisor: Dr Theodoros Georgiou

Description: Advanced sensor technologies are becoming smaller, cheaper, and more wearable. Monitoring a person’s motion during recovery and rehabilitation sessions can provide invaluable information informing health professionals as well as the patient themselves, of their progress markers.

The main aim of this PhD is to investigate the use of wearable sensors within the context of technology assisted rehabilitation.

This PhD project is highly interdisciplinary, and the successful PhD candidate will need to have a strong background in HCI methods and the ability to work with (and/or prototype) wearable sensors.

Please don't hesitate to contact me at T.Georgiou@hw.ac.uk for an informal discussion about this project and how our interests fit together.

IoT for independent living

Supervisor: Dr Theodoros Georgiou

Description: People for a variety of reasons may live on their own while still requiring access to health and care mechanisms. A “round the clock” carer may not be available through national health services or be within the budget of people needing them. Traditional monitoring devices such as cctv cameras, is also seen very rightfully by many as a big invasion of privacy.

The aim of this project is to develop a discrete IoT system of sensors that can infer activities of daily living when certain actions or series of actions are detected or completed. The successful PhD candidate will need to have a strong background in HCI methods. Strong motivation or the ability to design and make prototype sensors is desired.

Please don't hesitate to contact me at T.Georgiou@hw.ac.uk for an informal discussion about this project and how our interests fit together.

Hardware designs for high level declarative, managed, programming languages

Supervisor: Rob Stewart

Description: The performance of functional programming language implementations until 10-15 years ago enjoyed ncreasing clock frequencies on uni-core CPUs. Now, parallel computing is the only effective way to speed up computation. Due to a single bus connection from multiple cores on a CPU to main memory, functional languages with parallelism support are finding the limits of general purpose CPU architectures.

In recent times, the fabric on which we compute has changed fundamentally. Driven by the needs of AI, Big Data and energy efficiency, industry is moving away from general purpose CPUs to efficient special purpose hardware e.g. Google's Tensorflow Processing Unit (TPU) in 2016, Huawei's Neural Processing Unit (NPU) in smartphones, and Graphcore's Intelligent Processing Unit (IPU) in 2017. This reflects a wider shift to special purpose hardware to improve execution efficiency.

This PhD project will conduct research alongside the funded EPSRC project HAFLANG ( https://haflang.github.io ). The PhD student will have the choice on which architectural components to focus on. For example: 1) bespoke memory hierarchies for functional languages to minimise memory traffic where memory access latencies quickly become the bottleneck for real-world functional programs, or 2) lowering key runtime system components (prefetching, garbage collection, parallelism) into hardware to significantly reduce runtimes.

The aim of the PhD project will be to develop hardware/software co-design innovations in compiler construction and programmable hardware design that will 1) execute functional programs at least as twice as fast as on CPU architectures, and 2) consume four times less energy than CPUs when executing equivalent functional code. 

Runtime system innovations for non-strict managed functional languages

Supervisor: Rob Stewart

Description: High level functional languages offer the promise of programmer productivity, performance, and portability. Many languages hide hardware management from the programmer, e.g. memory allocation and evaluation order. A widely used language implementation is GHC, a software implementation of Haskell. The elegance of Haskell's non-strict evaluation strategy comes with a non-negligible overhead that presents a performance trade-off between avoiding unnecessary computation and runtime program management.

This PhD project will explore runtime system components that, if designed for modern architectures, have potential to significantly improve the efficiency of functional programming languages on stock hardware. The project will start by profiling cache misses, memory access latencies and memory contention to identify performance bottlenecks in real-world programs. The PhD project will use these profiles to design pre-fetching and locality aware garbage collection innovations for the GHC Haskell implementation to maximise the performance promises of non-strict evaluation strategies.

This project has significant potential for real-world impact with a large and growing Haskell community.

The project will complement the EPSRC HAFLANG project ( https://haflang.github.io ), which is mapping these architectural design ideas into modern day FPGA hardware technology.

Compressing robust deep learning models for Edge Computing

Supervisor: Rob Stewart

Description: There is a growing trend moving deep learning models from expensive GPUs towards Edge Computing devices such as embedded CPUs, mobile devices and programmable hardware. Trained neural networks require hundred of Gibabytes of memory and high computation resources. Emerging compression techniques are able to reduce those resource costs significantly. This not only affects the accuracy of neural networks, but also their robustness properties that make them vulnerable to attack or catastrophic predictions.

This PhD project will explore the design space of compression techniques applied to deep learning models, guided by neural network verification techniques. There will be a strong focus on scaling this design space to state-of-the-art real-world applications of neural networks. There is potential for this PhD project to have strong industrial engagement.

The outcomes of this PhD project will inform the research community and industry practitioners on how to construct reliable and efficient deep learning models for application domains such image processing smart cameras, autonomous robot, and driverless vehicles.

Type systems for secure IoT and smart devices

Supervisor: Rob Stewart

Description: Programmable hardware is increasingly used in IoT and embedded systems for smart home devices and safety critical systems. The correctness of hardware designs is therefore critical. When hardware components communicate, they must do so via an agreed protocol. Many hardware vendors provide proprietary IP blocks for use in System on Chip (SoC) implementations. How are we to trust the communication behaviours of third-party IP components?

This PhD project will investigate session types from programming language theory as a mechanism to construct trustworthy SoC designs and to verify the runtime behavioural correctness of proprietary third-party IP hardware. This project will build on the outcomes of the EPSRC Border Patrol project ( https://border-patrol.github.io ) .The project will develop mechanisms to translate session type descriptions into synthesisable monitoring hardware, and evaluate this technology on real-world SoC architectures. This PhD will be at the interface between programming language theory and real-world applications, with strong links with industry.

Zero-knowledge functional and parallel programming paradigms

Supervisor: Jamie Gabbay

Description: So-called zero-knowledge rollups (zk-rollups) work by executing computation on a (powerful) machine and delivering
* the result of the computation, and
* a cryptographic "certificate of honest execution" that the computation has been carried out correctly. 
What this means in practice is that computation in a distributed system (including but not limited to a blockchain) can safely be delegated, without every node in the distributed system having to run and re-run every computation.  They just check the certificates, which is simple and quick.

This is called "zero-knowledge (zk) computation" and "verifiable computation", and it is a mature field of research.

However, so far as I know what constitutes "computation" in this context has not been well-researched.  The models of computation used in practical zk systems are single-threaded Turing machines.  This works for some applications but breaks down if we require more powerful programming paradigms, such as functional programming (like Haskell, OCaml, Idris, or Agda), or inherently parallel computations (such as multiplication of large matrices).

The research goal can therefore be summed up as follows: given that "zk-Turing" exists, create "zk-Haskell" and "zk-CUDA".

Nominal tensor programming

Supervisor: Jamie Gabbay

Description: Nominal techniques were originally developed to model programming on syntax with binding (nominal abstract syntax), and have since been applied to other domains, most notably to automata (nominal automata).

A very natural next step is to examine graphs and tensors.  The act of connecting one node to another is viewed as a binding operation, where (literally) connecting two nodes binds those nodes together, but using nominal techniques this has a precise mathematical meaning.

The starting point of the project is to develop a theory of nominal graphs and tensor structures, and apply this in the mathematical fields of the candidate's choice.

Verification of AI/ Foundations for Verified AI

Supervisor: Ekaterina Komendantskaya

Description: Significant advances in Machine Learning led to its ubiquitous deployment in autonomous systems. However, Machine Learning is a black-box technology; therefore, any system that adopts it potentially jeopardises its safety, security, and interoperability. The significance of this problem has been recognised internationally, giving rise to EU AI Act and The Bletchley Park AI Declaration. For AI and autonomous systems like robots to be trusted we have ensure that they work for society in a responsible, verifiable, ethical, legal and safe manner.

In this PhD project, you will work in an interdisciplinary team that develops methods that combine formal verification, machine learning, and autonomous systems. A successful candidate is expected to have expertise in at least one of these domains. To see an example of the work that we do, consult this tutorial: https://vehicle-lang.github.io/tutorial/

Parallel runtime systems for high-performance machine learning

Supervisor: Hans-Wolfgang Loidl

Description: Parallel computation offers enhanced compute power by using a large number of independent compute units to solve a problem. Exploiting the potential of parallelism can be challenging when using low-level programming models such as C+MPI. In contrast, high-level languages, such as Haskell, provide abstractions to more easily implement parallel programs. Mapping these high-level abstractions down to the machine is the role of the runtime-system, and it has a lot of freedom how to efficiently arrange the parallel execution.

The core topic in this PhD is to develop and enhance parallel runtime systems for high-level languages, such as Haskell, Java, or Cilk, and improve the performance of parallel execution on multi-core servers as well as on compute clusters. The key challenges are to develop efficient scheduling and distribution technologies that work across a range of programs, and that are managed automatically by the runtime-system. The main application domain for these runtime-systems will be modern machine-learning algorithms with their high demands on data to be processed and compute units that should be exploited to make the ML technique feasible in real-world scenarios.

Algorithms in parallel symbolic computation

Supervisor: Hans-Wolfgang Loidl

Description: Symbolic computation covers a range of areas that apply mathematical knowledge to provide solutions for whole classes of problems. These typical focus on symbol manipulation over complex data structures, rather than numerical computation over flat structures such as matrices. Prominent sub-areas are computer algebra, with systems such as Maple or Mathematica, and automated theorem proving, with provers such as Isabelle or Coq. More recently this area is merging with the programming language area by supporting reasoning-oriented language features such as dependent types, with systems such as Agda.

The goal of this PhD thesis is to examine several commonly used symbolic algorithms and to investigate re-designs and re-implementations of these algorithms to cater for massive parallelism as is readily available now. The focus in this work could be on applying mathematical knowledge to re-design algorithms, using high-level language constructs to facilitate the parallelisation of existing algorithms, or on the verification of correctness and resource properties using modern verification techniques.

Type Error Diagnosis for Type Level Programming

Supervisor: Jurriaan Hage

Description: The Helium compiler for Haskell (see https://github.com/Helium4Haskell/) is a compiler that specializes in providing good type error diagnosis. Over the 2 decades since its inception we have made lots of progress, including work on GADTs and preliminary work on type families, but a few important parts of the Haskell programming language still need to be investigated: impredicative polymorphism/higher ranked types, and the many flavours of type classes that Haskell supports. Your task as a PhD is to consider these language extensions, implement them into the compiler, design heuristics, and validate the quality of these heuristics. Familiarity with Haskell is a definite plus, but do not worry if you have never used Haskell's many language extensions before.

Higher-rank polyvariance in static analysis of functional languages

Supervisor: Jurriaan Hage

Description: Higher-rank polyvariance (akin to higher-rank polymorphism in type systems) is a form of high precision for static analysis of functional languages. It is still unclear where the boundaries of decidability lie exactly, and your task to research where these lie more exactly by considering a number of static analyses and investigating what happens in these cases. Implementations can be made in the Helium compiler (https://github.com/Helium4Haskell/), or standalone implementations.

Another important aspect of higher-rank analysis is to ways to prove soundness of the analysis, preferably by mechanizing the meta-theory in Coq or some system like it.
Although implementation will form a sizable chunk of the work, this project makes high demands on your facilities of abstraction and your understanding of logical deduction systems, and is therefore quite mathematical in nature.

Reference: https://link.springer.com/chapter/10.1007/978-3-030-44914-8_24

SDN-based MANETs Using Existing OpenFlow Protocol

Supervisors: Idris Skloul Ibrahim and Lilia Georgievea

Description: There is a continuous business need for network technologies to increase functionality, performance, and complexity. However, the present network paradigms show a lack of adaptability and are limited to single-domain management. Thus, management of the network places a burden on the network’s users. In addition, the high number and variety of stationary or dynamic devices make the network massive and intractable, with a complexity that leads to scalability challenges. Modern requirements cannot be supported by the current decentralized mobile ad hoc networks (MANETs) standard models. Additionally, MANETs suffer from packets/network overheads due to topology changes with the distributed and (decentralized) routing in each node. In a typical architecture, the mobile node is responsible for dynamically detecting other nodes in the network. The node can communicate directly or via an intermediate node, and specify a route to other nodes. Thus, the node takes a decision with only a limited view of the network’s topology. To this end, the deployment of the Software Defined Networking (SDN) paradigm has the potential to enable the redesign of these models. SDN provides a global view of network topology and a programmable network with centralized management. In this paper, we propose a new architecture for SDN-based MANETs, which is adding an Open Virtual Switch (OVS) per node to find the effect of OVS on the MANETs performance. We present a practical implementation for the new architecture using the existing OpenFlow protocol. The tests have been carried out in an emulation environment based on Linux Containers (LXC V 2.0.11), Open Network Operating System (ONOS V 2.5.0) as a remote controller, NS3, and Open Virtual Switch (OVS V 2.5).

Programming with and Reasoning about Effect Handlers

Supervisor: Filip Sieczkowski

Description: Effect handlers are a novel way of structuring computational effects, and a focus of ongoing research into modular ways of incorporating effectful programming into functional programming. One of the approaches to do so, based on the notion of *lexically scoped* effects, is the foundation of a research programming language, Helium, originally developed at the University of Wrocław (https://bitbucket.org/pl-uwr/helium/).

While there is ongoing effort to provide some support for effect handlers in mainstream programming languages (OCaml 5.0, WebAssembly), there many challenges still remain, both in terms of practical support on the programming language side and the theoretical foundations of the paradigm. Depending on the interests of the PhD candidate, the topic can be skewed towards incorporating novel features and analyses in Helium, including developing more efficient compilation schemes, or towards investigation of theoretical background of effect handlers, for instance further developing the foundations for dependently typed programming with effect handlers.

Theory and Practice of Functorial Programming

Supervisor: Filip Sieczkowski

Description: Modern type systems for functional programming languages make ever increasing use of *type constructors*: the familiar lists and trees, classic algebraic datatypes, generalised to nested data types, GADTs and beyond. However, while the complexity of allowed type constructors increases, in most languages the only way to use them is by applying the type constructor to an argument to obtain a type: there are no programs related to the type constructors themselves. This is in stark contrast to some approaches to their semantics, which interpret the type constructors as *functors*, i.e., associate with each one an analogue of the "map" function for lists. Haskell can mimic this approach on a case-by-case basis by deriving an instance of the appropriate type class; however, this behaviour cannot be easily reflected when abstracting over a type constructor, and indeed, not all type constructors need to have associated instance of a Functor class.

This project is focused on exploring the design space of languages where all type constructors have associated functorial behaviour. This involves both language design aspects, such as integration of functorial type constructors and inductive/coinductive types, practical considerations and applications of functoriality to highly modular functional programming and data representation, as well as theoretical study of semantics of such languages, including questions of parametricity and equational reasoning in presence of functorial type constructors.

Domain Specific Logics for Interactive Theorem Proving

Supervisor: Filip Sieczkowski

Description: Most modern interactive theorem provers, particularly those based on type theory, implement a particular background logic that serves as the system's mathematical foundations. While the theory of choice is often very sophisticated and powerful, the user is bound to the logic and its attendant proof system. It is not so in pen-and-paper mathematics: we can easily use and re-use different approaches to syntax, including proof systems, depending on the task at hand. Often, this is achieved via *internal languages*, i.e., syntax that has canonical interpretation within any of a particular class of mathematical structures. Examples include simply-typed lambda calculus, which can be interpreted in any cartesian-closed category, or intuitionistic higher-order logic, which can be interpreted in any topos. Thus, one can build terms or prove theorems using different formation and proof rules, which may change from domain to domain. On the interactive theorem proving side, a similar approach has led to development of significant frameworks, including Iris (https://iris-project.org/), which expose a logic different to the background one to the user, and interpret the proofs as objects in the background logic. However, the syntax of such domain-specific logic cannot benefit from the system's proof management facilities, and is mostly achieved through sophisticated notation systems.

This project aims to explore approaches to integrating the DSL abstraction within an interactive theorem proving environment by modularising the proof system and allowing the user to connect models to their internal languages, in the process lifting the domain specific logic to the first-class status. This will involve both foundational theoretical work on modularising the syntax, and practical development of prototype implementations. There is also possibility for associated work in logic and theorem proving, including exploring non-standard approaches to equality in type theories.

Modularity in Proof Assistants

Supervisor: Kathrin Stark

Description: Today's world depends on safety- and security-critical software. In cases where software faults may have catastrophic results or the software has to withstand a determined attacker, a stronger guarantee than testing is desirable: formal verification. One promising approach is to develop mathematically-sound proofs that show that all inputs lead to the desired behaviour using interactive proof assistants.

However, despite their rising importance in academic and industrial settings, there is only little work on the modularity of their proofs. As a result, even small changes and extensions entail non-trivial code modifications. For example, proof assistants are commonly used to ensure the safety of domain-specific programming languages, i.e., programming languages tailored to a specific problem, by providing proofs about their metatheory, custom compilers, and correctness proofs for these custom compilers. Small modifications of the original language (e.g., extensions or partial use) require setting up a completely new code base.

This PhD project would investigate a new form of modularity for interactive definitions and proofs via open recursion and tailored tool support in the Coq proof assistant. If successful, this would allow extending code and proofs in hindsight. This would not only make existing developments much easier to maintain but also allow (as of now impossible) libraries of reusable language components.

Familiarity with a proof assistant is a definite plus; the project further possibly involves meta programming in Coq, e.g. with the MetaCoq tool.

Reference: https://www.ps.uni-saarland.de/Publications/documents/ForsterStark_2020_Coq.pdf

See my website (www.k-stark.de) for more information on what I do, and please don't hesitate to contact me at k.stark@hw.ac.uk to discuss how our interests fit together.

Mechanising Syntax with Binders

Supervisor: Kathrin Stark

Description: Mechanising binders in general-purpose proof assistants such as Coq is cumbersome and difficult. Yet binders, substitutions, and instantiation of terms with substitutions are critical ingredients of many programming languages. Any practicable mechanisation of the meta-theory of the latter hence requires a lean formalisation of the former.

The Autosubst project investigates the topic from three angles: First, it realises formal systems with binders based on both pure and scoped de Bruijn algebras together with basic syntactic rewriting lemmas and automation. It then automates this process in the Autosubst compiler, a tool that supports many-sorted, variadic, and modular syntax. Second, the choice of realisation and mechanise a proof of convergence of the σ-calculus, a calculus of explicit substitutions that is complete for equality of the de Bruijn algebra corresponding to the λ-calculus. Third, it demonstrates the practical usefulness of the approach by providing concise, transparent, and accessible mechanised proofs for a variety of case studies refined to de Bruijn substitutions.

I am looking for a PhD student interested in tackling one of many possible extensions/research questions. Examples include extensions to expressiveness such as intrinsically typed syntax, dependent predicates, (substitutive) functions, and dependent types or on the justification for more extensive syntax - but I'm also happy to discuss your ideas.

Familiarity with a proof assistant is a definite plus.

See my website (www.k-stark.de) for more information on what I do, and please don't hesitate to contact me at k.stark@hw.ac.uk to discuss how our interests fit together.

A Critical Enabler to Certifying Autonomous Systems 

Supervisor: Andrew Ireland 

Description: Safety critical autonomous systems, such as Unmanned Air Vehicles (UAVs) that operate beyond visual line of sight, require the highest level of certification. Certifiers are concerned with how such systems behave within their environment – as defined by system wide requirements, e.g. compliance with the rules-of-the-air [ SERA: https://www.caa.co.uk ]. Bridging the gap between system requirements and the code represents a major a challenge. Firstly, it requires a deep understanding of how the intended software should interact with the system as a whole in order that it delivers the required functionality within its operational environment. Secondly, such understandings need to be consistent and remain consistent right through to the code – if inconsistencies introduced at the early stage of a development go undetected, they can lead to catastrophic system failures, e.g. the loss of NASA’s Mars Polar Lander in 1999. System failures can also arise from incompleteness, i.e. missing requirements and missing constraints imposed by the environment. In general, mechanizing the detection of incompleteness is much harder than detecting inconsistencies. The investigation will seek to exploit synergies across the development process in order to highlight potential incompleteness, e.g. using anomalies observed at the level of a design simulation to question the completeness of the associated system requirements. While the primary aim of the project will be detection, a secondary aim will be to generate potential guidance as to how inconsistencies and incompleteness might be addressed. This will potentially improve the effectiveness and productivity of the designers and engineers, who must ultimately take responsibility for the integrity of the system. An added challenge is that many autonomous systems are an integration of opaque (i.e. machine-learned) and conventionally engineered components. The techniques developed within the project will need to take this into account. There exists an extensive literature in the areas of requirements engineering, formal methods and automated reasoning to build upon. Moreover, the project will benefit from strong collaborative links with D-RisQ Ltd [ https://www.drisq.com/ ] – a leading UK software and verification system provider. Specifically, the project will build upon the D-RisQ toolchain, which spans the analysis of system requirements right through to the verification of auto-generated code.  D-RisQ will also play a consultative role throughout the PhD project. In conclusion, the project is rich in research opportunities and has a strong industrial focus.  

UKRI AI Centre for Doctoral Training in Dependable and Deployable AI for Robotics (CDT-D2AIR)

The UKRI AI Centre for Doctoral Training in Dependable and Deployable AI for Robotics (CDT-D2AIR, pronounced "dare") is a joint 4-year PhD training programme offered by Heriot-Watt University and the University of Edinburgh through the Edinburgh Centre for Robotics. CDT-D2AIR will train students in the latest methods in AI, verification, design, and robotics, along with practical skills to ensure that robotic systems can be safely developed and deployed. The training programme combines state-of-the-art robotics, machine learning, optimisation, and software engineering with verification and testing. This training programme will be conducted within the context of emerging legal standards and regulations, sustainability, ethics, Responsible Research and Innovation (RRI), and Equality, Diversity, and Inclusion (EDI), all through engaging learning activities, to create a new generation of graduates working on dependable and deployable AI for robotics.

Find out more information about the UKRI AI Centre for Doctoral Training in Dependable and Deployable AI for Robotics.

EPSRC-funded PhD studentship

Heriot-Watt receives in the region of £1.5M per annum from the UK Research Councils to fund PhD research students. Awards to individuals comprise payment of fees and a non-taxable stipend of around £18,000 per annum (as of 2023). This is available to suitably qualified UK nationals and non-UK nationals if resident in the UK for 3 years prior to the course. Other EU students can apply to have fees paid only although Schools may be able to provide a partial stipend for highly qualified EU applicants.

 School Funded PhD Studentship

The School of Mathematical and Computer Sciences offers a number of full scholarships to both UK and international students, and the scholarship covers tuition fees at either international rate or UK rate and stipend (matching the EPSRC minimum stipend).

Information about research activities in each area can be found on the relevant group websites.

Further enquiries should be addressed to Dr Wei Pang.