# PhD Opportunities

SPLI coordinates events and networking opportunities for PhD students from all of our member institutions. Many academics at our member institutions are open to new PhD students in various areas related to Programming Languages research. Below we list possible supervisors from our member institutions as well as a brief description of their research interests.

If you are interested, please get in contact with a supervisor directly.

## University of Edinburgh

#### Ajitha Rajan

Software engineering, Software testing, Static analysis, Robustness and interpretability of AI models

#### Amir Shaikhha

Domain-specific languages, Databases, Compilers

#### Bjoern Franke

Compilers, JIT compilers, Parallelisation, Dynamic binary translation, Processor simulation, Software transformation driven by dynamic information

#### Chris Heunen

Foundations of quantum programming languages, Categorical semantics

#### David Aspinall

Software security and privacy, Theorem proving, Specification and verification

#### Don Sannella

Algebraic specification, Types and functional programming, Resource certification for mobile code

#### Elizabeth Polgreen

Program-synthesis methods and applications, Software verification

#### Ian Stark

Mathematical models for programming languages and concurrent systems

#### Jacques Fleuriot

Formal verification, Interactive theorem proving

#### James Cheney

Databases, Logic/Verification, Applications to provenance, Scientific-data management, Security

#### Markulf Kohlweiss

Formal verification of cryptographic-protocol designs and implementations

#### Mike O’Boyle

Compilers, Machine-learning-based compilation, Heterogeneous systems, Design space exploration

#### Myrto Arapinis

Provable security, including Verification of cryptographic protocols, Formal models, Protocol composition, Applied cryptography, Quantum cryptography with a particular interest in electronic voting

#### Ohad Kammar

Programming-language theory, Probabilistic programming, Meta programming, Category theory, Logic in Computer Science

#### Paul Jackson

Formal verification of hardware, software and cyber-physical systems, Interactive theorem proving

#### Perdita Stevens

Software engineering, Model-driven engineering

#### Peter Buneman

Query languages, Semistructured data, Data provenance

#### Philip Wadler

Functional programming, Agda, Gradual typing, Behavioural types

#### Rob van Glabbeek

Foundations of concurrency and distribution

#### Sam Lindley

Functional programming, Effect handlers, Behavioural types, Meta programming, Type inference, Expressiveness

## University of Glasgow

#### Blair Archibald

modelling concurrent systems, parallel functional programming

#### Colin Perkins

protocol specifications and standards

#### Gerardo Aragon Camarasa

programming languages for robotics

#### Gul Calikli

software engineering and programming languages

#### Jeremy Singer

managed runtime systems

#### Jose Cano Reyes

hardware-software co-design, edge computing

#### Michele Sevegnani

concurrent modelling languages

#### Ornela Dardha

behavioural types, mechanised programming language theory

#### Paul Harvey

runtime systems, adaptability, autonomous networks

#### Phil Trinder

parallel and distributed programming languages

#### Quintin Cutts

programming language education

#### Simon Fowler

functional programming, concurrent programming, behavioural types, multi-tier programming

#### Simon Gay

behavioural types, quantum programming languages

#### Wim Vanderbauwhede

programming language approaches to security, compilation to hardware, low-carbon and sustainable computing

## Heriot-Watt University

## University of St Andrews

#### Chris Brown

refactoring, energy-aware programming, parallel programming

#### Edwin Brady

dependent types, type-driven development, domain-specific languages, reasoning about effects

#### Ian Miguel

constraint modelling and solving

#### Olexandr Konovalov

programming language education, modelling

#### Özgür Akgün

domain-specific languages, constraint solutions, automated configuration

#### Ruth Hoffmann

domain-specific languages, models and symmetry reduction

#### Susmit Sarkar

formal architecture, memory consistency, compiler correctness

#### Tom Spink

compiler implementations, runtime systems, security

## University of Stirling

#### Patrick Maier

parallel and distributed programming languages, parallel symbolic computation, parallel cost models

## University of Strathclyde

#### Bob Atkey

formal analysis of programming languages via type theory, denotational semantics, and theorem provers

#### Clemens Kupke

Coalgebraic modelling of systems, Logical verification/model-checking, Fixpoint logics and their game-theoretic semantics, Logics for knowledge representation and databases, Automata theory

#### Conor McBride

dependent type theory, functional programming, effects and handlers, programming language design and metatheory, and the category theoretic underpinnings of all of the above

#### Fredrik Nordvall Forsberg

Dependent type theory, especially homotopy type theory, and its semantics and applications, Constructive mathematics, Categorical semantics of programming languages

#### Guillaume Allais

Type-driven programming, Correct-by-construction methodology, Proof automation, Generic programming, User experience of interactive compilers

#### Jan de Muijnck-Hughes

Applications of programming language theory and technologies (namely type systems, dependent types, and functional programming), to make systems more trustworthy

#### Jules Hedges

Applications of [category theory, type theory, functional programming, etc.] in [economics, machine learning, statistics, control, etc.]

#### Neil Ghani

Category theory, Type theory, Functional programming, Game theory, Machine learning

#### Radu Mardare

Logics for algebras and co-algebras, Quantitative algebraic reasoning, Approximation theories for systems, Reasoning about probabilistic and stochastic systems, Theories of bisimulation, Behavioural metrics, Metrics and topological approach to model theory

#### Ross Horne

Protocol verification (equivalence checking and privacy), Linked Data, Session Types and Proof Theory, Attack Trees, and Logic on Graphs

#### William Waites

Modelling of biological systems using process calculi, Applications of mathematics to public health, Generative models of synthetic populations, Low-carbon data collection for marine ecosystems and modelling thereof

## University of the West of Scotland

#### Paul Keir

compilers, heterogeneous systems, metaprogramming, functional programming