The school of Computer Science at the University of St Andrews has a fully-funded scholarship available working in the Programming Languages Research Group with Dr Christopher Brown. Applications must be received by 1 March 2025.
Background
Algorithmic skeletons provide a convenient and high-level approach to writing efficient parallel software by leveraging common patterns of parallel behaviours. A skeleton library presents the programmer with a library of high-level parallel interfaces, abstracting away the low-level complexities of manually handling concurrency primitives, e.g. locking, synchronisation and thread creation. Skeletons give an excellent compromise between ease of programming and the ability to generate highly efficient parallel software. A wide range of skeletons have been developed for several different languages, including Fastflow, TBB, PPL and OpenMP. However, despite the proliferation of skeleton libraries, there is little support for an increasingly popular class of programming languages equipped with dependent types.
Dependently-typed programming languages address the problem of program safety by ensuring that code conforms to its specification. This is achieved by permitting types to depend on values, thereby allowing programmers to express logical properties, and proof, as intrinsic parts of their programs. This conformance is checked at compile-time. This interest in dependent-types has resulted in a number of functional languages such as pi-forall, Agda, Idris and Coq. However, despite these developments in types, these dependently-typed languages still lack a parallel implementation, making development of safe parallel programs impossible.
This project will explore approaches to designing and implementing a dependently-typed parallel programming language. These approaches will consider the technical challenges, but also balancing those with the high-level usability that skeletons bring and the performance expectations of a performant system. As part of this exploration, use-cases will also need to be developed, and the scientific evaluation of the performance of the system will need to be carried out.
Topics of Interest
This project is largely exploratory in nature, and may take several different approaches and directions, including (but not limited to):
- Extending an existing dependently-typed language, such as Idris, with new concurrency primitives.
- Designing and implementing an efficient parallel runtime system as a backend to the language.
- Building on top of these primitives to provide dependently-typed concurrency behaviours, such as synchronisation points, channel behaviours, etc.
- To design and implement a set of dependently-typed algorithmic skeletons such as farms and pipelines.
- To explore and identify new skeletons that arise from writing dependently-typed programs.
- To use dependent-types to encode safety and soundness properties and reason about these properties in a formal way.
The Scholarship
We have one fully-funded scholarship available, starting in September 2025, which will be awarded to competitively to the best applicant. The scholarship covers all tuition fees (irrespective of country of origin) and comes with a stipend valued at £19,705 per annum. More details can be found here: https://blogs.cs.st-andrews.ac.uk/csblog/2024/10/24/phd-studentships-available-for-2025-entry/
International applications are welcome. We especially encourage female applicants and underrepresented minorities to apply. The School of Computer Science was awarded the Athena SWAN Silver award for its sustained progression in advancing equality and representation, and we welcome applications from those suitably qualified from all genders, all races, ethnicities and nationalities, LGBT+, all or no religion, all social class backgrounds, and all family structures to apply for our postgraduate research programmes.
To Apply
Informal enquiries can be directed to Chris. Full instructions for formal applications can be found at https://www.st-andrews.ac.uk/computer-science/prospective/pgr/how-to-apply/
The deadline for applications is 1 March 2025.