PhD opportunities in Computer Science

Supervisor: Mike Chantler 

Funding: £18,622 +£3,000 enhanced stipend/yr, 3.5yrs, fees paid

Description: This PhD will address the application of large language models and hierarchical topic modelling for interactive interpretation of massive knowledge repositories.

Advances in machine learning applied to natural language processing (NLP) are revolutionising our ability to search, find, understand and generate textual information.  This is an extraordinarily rapidly developing and exciting field of artificial intelligence (AI) research. 

There are two key areas where significant advancement has been made.  Firstly, training on massive, open, datasets for development of large language models (e.g., ChatGPT) and secondly, training in specialist technical fields where taxonomies, lexicons and semantics are a key part of the subject knowledge.  In these cases the natural control of specialist terminology provides key features to assist the development of machine learning models and the use of AI assistance in processing and understanding large unstructured document sets. 

Many technical fields exhibit a less controlled, ambiguous terminology set where context may change the semantics of the terms; the subject field being defined via the topics addressed.  The development of topic models for these specialist fields is important when seeking to search, discover and contextualise analysis of document copra.  Such topic models provide critical context which enhances our ability to understand and efficiently obtain value from these document sets. 

Being able to build and define such rich topic models is expected to aid additional natural language processing (NLP) tools in searching, separating and understanding document content and provide thematic overviews of these repositories. 

This project seeks to research the ability to form these topic models in narrow technical fields using large language models and classical machine learning techniques, and then use and embed them within additional NLP tools to digest, understand, search and sort documentation sets. 

Eligibility: This scholarship is available only to ‘home’ students. To be treated as a home student, candidates must meet one of these criteria:

• be a UK national (meeting residency requirements)
• have settled status
• have pre-settled status (meeting residency requirements)
• have indefinite leave to remain or enter.

Further Information: Enhanced PhD Scholarship in Machine Learning

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

Enhanced PhD Scholarship in Machine Learning

Supervisor: Mike Chantler 

Funding: £18,622 +£3,000 enhanced stipend/yr, 3.5yrs, fees paid

Description: This PhD will address the application of large language models and hierarchical topic modelling for interactive interpretation of massive knowledge repositories.

Advances in machine learning applied to natural language processing (NLP) are revolutionising our ability to search, find, understand and generate textual information.  This is an extraordinarily rapidly developing and exciting field of artificial intelligence (AI) research. 

There are two key areas where significant advancement has been made.  Firstly, training on massive, open, datasets for development of large language models (e.g., ChatGPT) and secondly, training in specialist technical fields where taxonomies, lexicons and semantics are a key part of the subject knowledge.  In these cases the natural control of specialist terminology provides key features to assist the development of machine learning models and the use of AI assistance in processing and understanding large unstructured document sets. 

Many technical fields exhibit a less controlled, ambiguous terminology set where context may change the semantics of the terms; the subject field being defined via the topics addressed.  The development of topic models for these specialist fields is important when seeking to search, discover and contextualise analysis of document copra.  Such topic models provide critical context which enhances our ability to understand and efficiently obtain value from these document sets. 

Being able to build and define such rich topic models is expected to aid additional natural language processing (NLP) tools in searching, separating and understanding document content and provide thematic overviews of these repositories. 

This project seeks to research the ability to form these topic models in narrow technical fields using large language models and classical machine learning techniques, and then use and embed them within additional NLP tools to digest, understand, search and sort documentation sets. 

Eligibility: This scholarship is available only to ‘home’ students. To be treated as a home student, candidates must meet one of these criteria:

• be a UK national (meeting residency requirements)
• have settled status
• have pre-settled status (meeting residency requirements)
• have indefinite leave to remain or enter.

Further Information: Enhanced PhD Scholarship in Machine Learning

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.

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: Predictions and judgements made by machine learning algorithms play an increasingly important role in complex intelligent applications in society-spanning critical sectors such as economics, manufacture, energy, legislation, healthcare, and security. Because of the impact of these decisions, it is of central importance to understand what factors contributed to a decision, or whether trust in a decision can be significantly improved.

Historically, a particularly influential approach is Valiant’s learnability theory, which in the 1980s gave abstract theoretical foundations for supervised machine learning. These foundations provided theoretical methods to bound accuracy of classifiers on the training data, and measure how they generalise to yet unseen examples.

However, a more recent realisation, due to Szegedy et al., is that even complex ("deep") networks with high accuracy and generalisation capacity fall victims to adversarial attacks (extremely small perturbations to the inputs). This is not just a security issue for practical applications of neural networks, but it uncovers a much bigger problem: accuracy and generalisation measures do not characterise how well the network learnt “semantic meaning” of classes. Subsequent research introduced different ways to train networks to be robust (e.g. data augmentation, adversarial training), which however were still vulnerable to a strong enough attack. Moreover, it was shown that other kinds of ML have the same vulnerabilities, notably reinforcement learning, recurrent networks and transformers. There is a growing understanding within the community that machine learning needs new foundations in order to tackle this problem of AI verification.

At the same time, the well-established verification technologies (SMT solvers, model checkers, higher-order interactive theorem provers) that have seen successes in standard software verification often fail to apply out-of-the box in machine learning scenarios. Lab for AI and Verification (www.laiv.uk) at Heriot-Watt is a group of reserachers working on better understanding of the verification challenge that complex intelligent systems pose and on methods of adapting logic, functional programming, type theory methodologies in this new domain. See our webpage for examples of concrete projects and contact ek19@hw.ac.uk to discuss how your interests fit with LAIV.

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.

EPSRC Centre for Doctoral Training Award (Robotics and Autonomous Systems)

The Centre's main programme is the EPSRC Centre for Doctoral Training in Robotics and Autonomous Systems. Its goal is to train innovation-ready robotics researchers to be part of a multi-disciplinary enterprise, requiring sound knowledge of physics (kinematics, dynamics), engineering (control, signal processing, mechanical design), computer science (algorithms for perception, planning, decision making and intelligent behaviour, software engineering), as well as allied areas ranging from biology and biomechanics to cognitive psychology.

Find out more information about the EPSRC Centre for Doctoral Training in Robotics and Autonomous Systems.

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.